From 60443f2093184dc5a97d816e775847ae95915a2f Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Thu, 20 Jun 2024 14:05:43 +0200 Subject: [PATCH] Fix the build instruction --- README.md | 16 +++------------- meta.yml | 11 +++++++++++ 2 files changed, 14 insertions(+), 13 deletions(-) diff --git a/README.md b/README.md index 218480a..8a737a3 100644 --- a/README.md +++ b/README.md @@ -68,25 +68,15 @@ slices in the input. - [A bargain for mergesorts (functional pearl) — How to prove your mergesort correct and stable, almost for free](https://arxiv.org/abs/2403.08173) doi:[10.48550/arXiv.2403.08173](https://doi.org/10.48550/arXiv.2403.08173) ## Building and installation instructions - -The easiest way to install the latest released version of Stable sort algorithms in Coq +The easiest way to install the development version of Stable sort algorithms in Coq is via [OPAM](https://opam.ocaml.org/doc/Install.html): - -```shell -opam repo add coq-released https://coq.inria.fr/opam/released -opam install coq-stablesort -``` - -To instead build and install manually, do: - ``` shell git clone https://github.com/pi8027/stablesort.git cd stablesort -make # or make -j -make install +opam repo add coq-released https://coq.inria.fr/opam/released +opam install ./coq-stablesort.opam ``` - ## Credits The mergesort functions and the stability proofs provided in this library are mostly based on ones in the `path` library of Mathematical Components. diff --git a/meta.yml b/meta.yml index b085f55..4dcfac7 100644 --- a/meta.yml +++ b/meta.yml @@ -186,6 +186,17 @@ action_appendix: |2- env: OPAMWITHTEST: true +build: |- + ## Building and installation instructions + The easiest way to install the development version of Stable sort algorithms in Coq + is via [OPAM](https://opam.ocaml.org/doc/Install.html): + ``` shell + git clone https://github.com/pi8027/stablesort.git + cd stablesort + opam repo add coq-released https://coq.inria.fr/opam/released + opam install ./coq-stablesort.opam + ``` + documentation: |- ## Credits The mergesort functions and the stability proofs provided in this library are