From 7337e5e06e8f2031b93eccf158eb0093eafc8335 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Sun, 15 Nov 2020 21:41:53 +0100 Subject: [PATCH] docs: Final edits for the CEP 48 --- text/048-packaging-coq-native.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/text/048-packaging-coq-native.md b/text/048-packaging-coq-native.md index 9ad2c20..1623602 100644 --- a/text/048-packaging-coq-native.md +++ b/text/048-packaging-coq-native.md @@ -25,11 +25,11 @@ Also, this proposal makes the configuration uniform across the platforms (while The proposal is three-fold: -* **item 1.** Update the `coq` packaging in `opam-repository` so that Coq's standard library is compiled with `-native-compiler no` by default, unless an additional meta-package `coq-native` has been installed by the user. +* **item 1.** Update the `coq` packaging in [ocaml/opam-repository](https://github.com/ocaml/opam-repository) so that Coq's standard library is compiled with `-native-compiler no` by default, unless an additional meta-package `coq-native` has been installed by the user. * **item 2.** Extend the `./configure -native-compiler` options: * option `./configure -native-compiler yes` now impacts the default value of option `coqc -native-compiler` (in order to precompile both stdlib and third-party libraries with `-native-compiler yes`); * option `-native-compiler ondemand` (which becomes the default when compiling coq manually) preserves the previous default behavior (modulo the stdlib that is not precompiled anymore). -* **item 3.** Optionally: to enhance `native_compute` support with old versions of Coq (the releases of Coq before 8.13 where **item 2** is implemented), update the `opam` packacking of the considered libraries. +* **item 3.** Optionally: to enhance `native_compute` support with old versions of Coq (the releases of Coq before 8.13 where **item 2** is implemented), update the `opam` packaging of the considered libraries. ## Regarding item 1: @@ -100,7 +100,7 @@ index fdb19e9da7..3d3dee7570 100644 The `coqc` option `-native-compiler ondemand` corresponds to the default behavior since [4ad6855](https://github.com/coq/coq/commit/4ad6855504db2ce15a474bd646e19151aa8142e2) (8.5beta3). -The following tabular, adapted from [this coq/coq#12564 comment](https://github.com/coq/coq/issues/12564#issuecomment-647464937), summarizes all behaviors (the changes are highlighted in bold): +The following array, adapted from [this coq/coq#12564 comment](https://github.com/coq/coq/issues/12564#issuecomment-647464937), summarizes all behaviors (the changes are highlighted in bold): | `configure (<8.13)` | `configure (>=8.13)` | `coqc` | outcome | | --- | --- | --- | --- | @@ -136,7 +136,7 @@ diff --git a/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.1.10.0/opam depends: [ "coq" { (>= "8.7" & < "8.12~") } ] ``` -Doing this, one can notice that the appropriate `.coq-native` directory has succesfully been installed along the `.vo` of the library: +Doing this, one can notice that the appropriate `.coq-native` directory has successfully been installed along the `.vo` of the library: ```bash find "$(opam config var lib)" -name ".coq-native" | grep ssreflect @@ -147,13 +147,13 @@ find "$(opam config var lib)" -name ".coq-native" | grep ssreflect To fully benefit from `native_compute` with a library using Coq 8.5+, some (`opam`) packaging update may be required for this library's dependencies: - for `coq_makefile`: no change required for Coq 8.13+; otherwise follow **item 3** above (related to Section [Precompiling for `native_compute`](https://coq.github.io/doc/master/refman/practical-tools/utilities.html?highlight=coq_makefile#precompiling-for-native-compute) in Coq refman); -- for `dune / coq.theory`: this will require Coq 8.12.1+ and a version of `dune` implementing [PR ocaml/dune#3210](https://github.com/ocaml/dune/pull/3210) (cf. [this comment](https://github.com/coq/ceps/pull/48#issuecomment-727020253) by **@ejgallego**) +- for `dune / coq.theory`: this will require Coq 8.12.1+ and a version of `dune` implementing [PR ocaml/dune#3210](https://github.com/ocaml/dune/pull/3210) (cf. [this comment](https://github.com/coq/ceps/pull/48#issuecomment-727020253) by **@ejgallego**); otherwise (without native support), Dune will just ignore the native parts and no `./coq-native/*.cmxs` file will be installed. Note that these changes could be performed directly in the existing packages gathered in the [coq/opam-coq-archive](https://github.com/coq/opam-coq-archive) repository. # Alternatives -* A different but related idea was mentioned in [Zulip](https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs.20.26.20plugin.20devs/topic/Coq-as-compiler): "OPAM: try out coq as a compiler" ([PR coq/opam-coq-archive#595](https://github.com/coq/opam-coq-archive/issues/595)). +* A different but related idea was mentioned in [Zulip](https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs.20.26.20plugin.20devs/topic/Coq-as-compiler/near/216196895): "OPAM: try out coq as a compiler" ([PR coq/opam-coq-archive#595](https://github.com/coq/opam-coq-archive/issues/595)). * This would require opam 2.0 (which is not a drawback). * This could be viewed as an alternative of this CEP's package flag. * Unfortunately, this alternative would be even coarser than this CEP (as all opam packages, not only those of coq libraries, would be recompiled). @@ -175,4 +175,4 @@ Note that these changes could be performed directly in the existing packages gat * This CEP was discussed at the 2020-11-13 weekly Coq call, in order to provide full-blown `native_compute` support for the Coq 8.13 release (cf. [PR coq/coq#13352](https://github.com/coq/coq/pull/13352)). * The Coq team agreed on considering this CEP for Coq 8.13, while the `split-native` strategy could be further developed for a later Coq release. -*Note:* at the time this CEP is written, the Coq refman still lacks some documentation of the `-native-compiler` option; but progress on this is tracked in issue [coq/coq#12564](https://github.com/coq/coq/issues/12564). +*Note:* at the time this CEP is written, the Coq refman still lacks some documentation of the `-native-compiler` option; but progress on this is tracked in issue [coq/coq#12564](https://github.com/coq/coq/issues/12564); and that doc might incorporate [the array above](#regarding-item-2).