[coq] Add (boot) library field to handle Coq's stdlib bootstrap.#3096
[coq] Add (boot) library field to handle Coq's stdlib bootstrap.#3096aalekseyev merged 2 commits intoocaml:masterfrom
(boot) library field to handle Coq's stdlib bootstrap.#3096Conversation
|
I can't vouch for correctness of coq rules, but the patch seems reasonable at a first glance: it does not change the existing behavior and hardcoding "Init" I think is totally fine if that's also hard-coded in Coq. I invite you to try running the build with sandboxing (--sandbox=copy) to make sure you're not missing some dependencies. |
Thanks a lot for the review @aalekseyev ; I expect some churn in Coq advanced support tho, unfortunately Coq toolchain has a few quirks and its cleanup depends on getting the bootstrap fully working with Dune first; I am trying to manage the best we can. At some point when things are stable we will declare version 1.0 of the coq stanzas and remove support for 0.1 .
Oh, I didn't know of this mode, it seems very useful thanks! And indeed it catches a problem, the first call to coqdep makes dune hang; the deps look correct tho; so I am betting of a bug in coqdep parsing, which indeed should be made more resilient. |
|
The problem seems more in the way I pass the OCaml include flags to |
|
From what I've seen yesterday, it seems that:
I think a reasonable solution should be to use I agree the issue exists in master, though. If you find time to look at it, it would be appreciated, but it doesn't have to block this PR. |
We add an experimental `boot` field to the `coq.theory` stanza to mark that the theory being compiled includes Coq's prelude. When building the Coq prelude [or it is in scope in a composed build], we must perform two special things: - the implicit dependency on `Init.Prelude.vo` must be reflected the - location of prelude's build artifacts has to passed using `-coqlib`, as Coq heuristics to locate it will fail There is a small hack in this PR, which is the special handling of the `Init` library prefix, once we implement per-file flags that could be relaxed; it doesn't matter much as both `Init` and `Init.Prelude` are hardcoded into Coq as of today [we will likely lift this restriction in a 2.0 coq language version] Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
|
Thanks for the review @aalekseyev ; I've actually queued a modification to |
|
Given the restricted scope of this PR I propose to merge tomorrow. |
…lugin, dune-private-libs and dune-glob (2.3.0) CHANGES: - Improve validation and error handling of arguments to `dune init` (ocaml/dune#3103, fixes ocaml/dune#3046, @shonfeder) - `dune init exec NAME` now uses the `NAME` argument for private modules (ocaml/dune#3103, fixes ocaml/dune#3088, @shonfeder) - Avoid linear walk to detect children, this should greatly improve performance when a target has a large number of dependencies (ocaml/dune#2959, @ejgallego, @aalekseyev, @Armael) - [coq] Add `(boot)` option to `(coq.theories)` to enable bootstrap of Coq's stdlib (ocaml/dune#3096, @ejgallego) - [coq] Deprecate `public_name` field in favour of `package` (ocaml/dune#2087, @ejgallego) - Better error reporting for "data only" and "vendored" dirs. Using these with anything else than a strict subdirectory or `*` will raise an error. The previous behavior was to just do nothing (ocaml/dune#3056, fixes ocaml/dune#3019, @voodoos) - Fix bootstrap on bytecode only switches on windows or where `-j1` is set. (ocaml/dune#3112, @xclerc, @rgrinberg) - Allow `enabled_if` fields in `executable(s)` stanzas (ocaml/dune#3137, fixes ocaml/dune#1690 @voodoos) - Do not fail if `ocamldep`, `ocamlmklib`, or `ocaml` are absent. Wait for them to be used to fail (ocaml/dune#3138, @rgrinberg) - Introduce a `strict_package_deps` mode that verifies that dependencies between packages in the workspace are specified correctly. (@rgrinberg, ocaml/dune#3117)
…lugin, dune-private-libs and dune-glob (2.3.0) CHANGES: - Improve validation and error handling of arguments to `dune init` (ocaml/dune#3103, fixes ocaml/dune#3046, @shonfeder) - `dune init exec NAME` now uses the `NAME` argument for private modules (ocaml/dune#3103, fixes ocaml/dune#3088, @shonfeder) - Avoid linear walk to detect children, this should greatly improve performance when a target has a large number of dependencies (ocaml/dune#2959, @ejgallego, @aalekseyev, @Armael) - [coq] Add `(boot)` option to `(coq.theories)` to enable bootstrap of Coq's stdlib (ocaml/dune#3096, @ejgallego) - [coq] Deprecate `public_name` field in favour of `package` (ocaml/dune#2087, @ejgallego) - Better error reporting for "data only" and "vendored" dirs. Using these with anything else than a strict subdirectory or `*` will raise an error. The previous behavior was to just do nothing (ocaml/dune#3056, fixes ocaml/dune#3019, @voodoos) - Fix bootstrap on bytecode only switches on windows or where `-j1` is set. (ocaml/dune#3112, @xclerc, @rgrinberg) - Allow `enabled_if` fields in `executable(s)` stanzas (ocaml/dune#3137, fixes ocaml/dune#1690 @voodoos) - Do not fail if `ocamldep`, `ocamlmklib`, or `ocaml` are absent. Wait for them to be used to fail (ocaml/dune#3138, @rgrinberg) - Introduce a `strict_package_deps` mode that verifies that dependencies between packages in the workspace are specified correctly. (@rgrinberg, ocaml/dune#3117) - Make sure the `@all` alias is defined when no `dune` file is present in a directory (ocaml/dune#2946, fix ocaml/dune#2927, @diml)
…lugin, dune-private-libs and dune-glob (2.3.0) CHANGES: - Improve validation and error handling of arguments to `dune init` (ocaml/dune#3103, fixes ocaml/dune#3046, @shonfeder) - `dune init exec NAME` now uses the `NAME` argument for private modules (ocaml/dune#3103, fixes ocaml/dune#3088, @shonfeder) - Avoid linear walk to detect children, this should greatly improve performance when a target has a large number of dependencies (ocaml/dune#2959, @ejgallego, @aalekseyev, @Armael) - [coq] Add `(boot)` option to `(coq.theories)` to enable bootstrap of Coq's stdlib (ocaml/dune#3096, @ejgallego) - [coq] Deprecate `public_name` field in favour of `package` (ocaml/dune#2087, @ejgallego) - Better error reporting for "data only" and "vendored" dirs. Using these with anything else than a strict subdirectory or `*` will raise an error. The previous behavior was to just do nothing (ocaml/dune#3056, fixes ocaml/dune#3019, @voodoos) - Fix bootstrap on bytecode only switches on windows or where `-j1` is set. (ocaml/dune#3112, @xclerc, @rgrinberg) - Allow `enabled_if` fields in `executable(s)` stanzas (ocaml/dune#3137, fixes ocaml/dune#1690 @voodoos) - Do not fail if `ocamldep`, `ocamlmklib`, or `ocaml` are absent. Wait for them to be used to fail (ocaml/dune#3138, @rgrinberg) - Introduce a `strict_package_deps` mode that verifies that dependencies between packages in the workspace are specified correctly. (@rgrinberg, ocaml/dune#3117) - Make sure the `@all` alias is defined when no `dune` file is present in a directory (ocaml/dune#2946, fix ocaml/dune#2927, @diml)
We add an experimental
bootfield to thecoq.theorystanza to markthat the theory being compiled includes Coq's prelude.
When building the Coq prelude [or it is in scope in a composed build],
we must perform two special things:
Init.Prelude.vomust be reflected-coqlib,as Coq heuristics to locate it will fail
There is a small hack in this PR, which is the special handling of the
Initlibrary prefix, once we implement per-file flags that could berelaxed; it doesn't matter much as both
InitandInit.Preludearehardcoded into Coq as of today [we will likely lift this restriction
in a 2.0 coq language version]