-
Notifications
You must be signed in to change notification settings - Fork 413
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feature(coq): coq macro #6049
feature(coq): coq macro #6049
Conversation
c554b3b
to
8dbdbcd
Compare
@ejgallego ping |
503e61b
to
70b0eb8
Compare
Looks very good to me, thanks! I can do a full code review next week after I'm done with the Sabanci class, but if someone else wants to take over, the interface for this PR looks good to me so you can merge. Need to update the docs and changelog I think. |
Also It is a hack so people could have coq_makefile output native files just by recompiling coq. |
We can name it whatever we want, I just kept the env var name from configure. |
@ejgallego ping |
(run sed "/^CAMLFLAGS=/d") | ||
(run sed "/^WARN=/d") | ||
(run sed "/^HASNATDYNLINK=/d") | ||
(run sed "/^COQ_SRC_SUBDIRS=/d")) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe you want to use grep to filter out the positive ones instead (use the egrep |
pattern for disjunctive regexps)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Grep might not run the same in mac so I stuck to sed
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks very good to me but I'm not expert on the expander code, so it'd be nice if an expert could have a look, maybe (@rgrinberg ) ?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Actually CHANGES and doc need updating.
@ejgallego I've added a changelog and some doc. |
The expander code is originally @rgrinberg's, but if he has some time, I wouldn't mind another pair of eyes. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Mostly minor grammar/formatting suggestions. One question at the end about phrasing.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Great, will merge once the conflict is solved.
Signed-off-by: Ali Caglayan <alizter@gmail.com>
Signed-off-by: Ali Caglayan <alizter@gmail.com>
Signed-off-by: Ali Caglayan <alizter@gmail.com>
…ne-site, dune-rpc, dune-rpc-lwt, dune-private-libs, dune-glob, dune-configurator, dune-build-info, dune-action-plugin and chrome-trace (3.5.0~alpha1) CHANGES: - Sandbox running cinaps actions starting from cinaps 1.1 (ocaml/dune#6176, @rgrinberg) - Add a `runtime_deps` field in the `cinaps` stanza to specify runtime dependencies for running the cinaps preprocessing action (ocaml/dune#6175, @rgrinberg) - Shadow alias module `Foo__` when building a library `Foo` (ocaml/dune#6126, @rgrinberg) - Extend dune describe to include the root path of the workspace and the relative path to the build directory. (ocaml/dune#6136, @reubenrowe) - Allow dune describe workspace to accept directories as arguments. The provided directories restrict the worskpace description to those directories. (ocaml/dune#6107, fixes ocaml/dune#3893, @esope) - Add a terminal persistence mode that attempts to clear the terminal history. It is enabled by setting terminal persistence to `clear-on-rebuild-and-flush-history` (ocaml/dune#6065, @rgrinberg) - Disallow generating targets in sub direcories in inferred rules. The check to forbid this was accidentally done only for manually specified targets (ocaml/dune#6031, @rgrinberg) - Do not ignore rules marked `(promote (until-clean))` when `--ignore-promoted-rules` (or `-p`) is passed. (ocaml/dune#6010, fixes ocaml/dune#4401, @emillon) - Dune no longer considers .aux files as targets during Coq compilation. This means that .aux files are no longer cached. (ocaml/dune#6024, fixes ocaml/dune#6004, @Alizter) - Cinaps actions are now sandboxed by default (ocaml/dune#6062, @rgrinberg) - Allow rules producing directory targets to be not sandboxed (ocaml/dune#6056, @rgrinberg) - Introduce a `dirs` field in the `install` stanza to install entire directories (ocaml/dune#5097, fixes ocaml/dune#5059, @rgrinberg) - Menhir rules are now sandboxed by default (ocaml/dune#6076, @rgrinberg) - Allow rules producing directory targets to create symlinks (ocaml/dune#6077, fixes ocaml/dune#5945, @rgrinberg) - Inline tests are now sandboxed by default (ocaml/dune#6079, @rgrinberg) - Fix build-info version when used with flambda (ocaml/dune#6089, fixes ocaml/dune#6075, @jberdine) - Add an `(include <file>)` term to the `include_dirs` field for adding directories to the include paths sourced from a file. (ocaml/dune#6058, fixes ocaml/dune#3993, @gridbugs) - Support `(extra_objects ...)` field in `(executable ...)` and `(library ...)` stanzas (ocaml/dune#6084, fixes ocaml/dune#4129, @gridbugs) - Fix compilation of Dune under esy on Windows (ocaml/dune#6109, fixes ocaml/dune#6098, @nojb) - Improve error message when parsing several licenses in `(license)` (ocaml/dune#6114, fixes ocaml/dune#6103, @emillon) - odoc rules now about `ODOC_SYNTAX` and will rerun accordingly (ocaml/dune#6010, fixes ocaml/dune#1117, @emillon) - dune install: copy files in an atomic way (ocaml/dune#6150, @emillon) - Add `%{coq:...}` macro for accessing data about the configuration about Coq. For instance `%{coq:version}` (ocaml/dune#6049, @Alizter) - update vendored copy of cmdliner to 1.1.1. This improves the built-in documentation for command groups such as `dune ocaml`. (ocaml/dune#6038, @emillon, ocaml/dune#6169, @shonfeder) - The test suite for Coq now requires Coq >= 8.16 due to changes in the plugin loading mechanism upstream (which now uses findlib). - Starting with Coq build language 0.6, theories can be built without importing Coq's standard library by including `(stdlib no)`. (ocaml/dune#6165 ocaml/dune#6164, fixes ocaml/dune#6163, @ejgallego @Alizter @LasseBlaauwbroek) - on macOS, sign executables produced by artifact substitution (ocaml/dune#6137, fixes ocaml/dune#5650, @emillon) - Added an (aliases ...) field to the (rules ...) stanza which allows the specification of multiple aliases per rule (ocaml/dune#6194, @Alizter)
…ne-site, dune-rpc, dune-rpc-lwt, dune-private-libs, dune-glob, dune-configurator, dune-build-info, dune-action-plugin and chrome-trace (3.5.0) CHANGES: - macOS: Handle unknown fsevents without crashing (ocaml/dune#6217, @rgrinberg) - Enable file watching on MacOS SDK < 10.13. (ocaml/dune#6218, @rgrinberg) - Sandbox running cinaps actions starting from cinaps 1.1 (ocaml/dune#6176, @rgrinberg) - Add a `runtime_deps` field in the `cinaps` stanza to specify runtime dependencies for running the cinaps preprocessing action (ocaml/dune#6175, @rgrinberg) - Shadow alias module `Foo__` when building a library `Foo` (ocaml/dune#6126, @rgrinberg) - Extend dune describe to include the root path of the workspace and the relative path to the build directory. (ocaml/dune#6136, @reubenrowe) - Allow dune describe workspace to accept directories as arguments. The provided directories restrict the worskpace description to those directories. (ocaml/dune#6107, fixes ocaml/dune#3893, @esope) - Add a terminal persistence mode that attempts to clear the terminal history. It is enabled by setting terminal persistence to `clear-on-rebuild-and-flush-history` (ocaml/dune#6065, @rgrinberg) - Disallow generating targets in sub direcories in inferred rules. The check to forbid this was accidentally done only for manually specified targets (ocaml/dune#6031, @rgrinberg) - Do not ignore rules marked `(promote (until-clean))` when `--ignore-promoted-rules` (or `-p`) is passed. (ocaml/dune#6010, fixes ocaml/dune#4401, @emillon) - Dune no longer considers .aux files as targets during Coq compilation. This means that .aux files are no longer cached. (ocaml/dune#6024, fixes ocaml/dune#6004, @Alizter) - Cinaps actions are now sandboxed by default (ocaml/dune#6062, @rgrinberg) - Allow rules producing directory targets to be not sandboxed (ocaml/dune#6056, @rgrinberg) - Introduce a `dirs` field in the `install` stanza to install entire directories (ocaml/dune#5097, fixes ocaml/dune#5059, @rgrinberg) - Menhir rules are now sandboxed by default (ocaml/dune#6076, @rgrinberg) - Allow rules producing directory targets to create symlinks (ocaml/dune#6077, fixes ocaml/dune#5945, @rgrinberg) - Inline tests are now sandboxed by default (ocaml/dune#6079, @rgrinberg) - Fix build-info version when used with flambda (ocaml/dune#6089, fixes ocaml/dune#6075, @jberdine) - Add an `(include <file>)` term to the `include_dirs` field for adding directories to the include paths sourced from a file. (ocaml/dune#6058, fixes ocaml/dune#3993, @gridbugs) - Support `(extra_objects ...)` field in `(executable ...)` and `(library ...)` stanzas (ocaml/dune#6084, fixes ocaml/dune#4129, @gridbugs) - Fix compilation of Dune under esy on Windows (ocaml/dune#6109, fixes ocaml/dune#6098, @nojb) - Improve error message when parsing several licenses in `(license)` (ocaml/dune#6114, fixes ocaml/dune#6103, @emillon) - odoc rules now about `ODOC_SYNTAX` and will rerun accordingly (ocaml/dune#6010, fixes ocaml/dune#1117, @emillon) - dune install: copy files in an atomic way (ocaml/dune#6150, @emillon) - Add `%{coq:...}` macro for accessing data about the configuration about Coq. For instance `%{coq:version}` (ocaml/dune#6049, @Alizter) - update vendored copy of cmdliner to 1.1.1. This improves the built-in documentation for command groups such as `dune ocaml`. (ocaml/dune#6038, @emillon, ocaml/dune#6169, @shonfeder) - The test suite for Coq now requires Coq >= 8.16 due to changes in the plugin loading mechanism upstream (which now uses `Findlib`). - Starting with Coq build language 0.6, theories can be built without importing Coq's standard library by including `(stdlib no)`. (ocaml/dune#6165 ocaml/dune#6164, fixes ocaml/dune#6163, @ejgallego @Alizter @LasseBlaauwbroek) - on macOS, sign executables produced by artifact substitution (ocaml/dune#6137, ocaml/dune#6231, fixes ocaml/dune#5650, fixes ocaml/dune#6226, @emillon) - Added an (aliases ...) field to the (rules ...) stanza which allows the specification of multiple aliases per rule (ocaml/dune#6194, @Alizter) - The `(coq.theory ...)` stanza will now ensure that for each declared `(plugin ...)`, the `META` file for it is built before calling `coqdep`. This enables the use of the new `Findlib`-based loading method in Coq 8.16; however as of Coq 8.16.0, Coq itself has some bugs preventing this to work yet. (ocaml/dune#6167 , workarounds ocaml/dune#5767, @ejgallego) - Allow include statement in install stanza (ocaml/dune#6139, fixes ocaml/dune#256, @gridbugs) - Handle CSI n K code in ANSI escape codes from commands. (ocaml/dune#6214, fixes ocaml/dune#5528, @emillon) - Add a new experimental feature `mode_specific_stubs` that allows the specification of different flags and sources for foreign stubs depending on the build mode (ocaml/dune#5649, @voodoos)
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be Signed-off-by: Ali Caglayan <alizter@gmail.com>
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be Signed-off-by: Ali Caglayan <alizter@gmail.com>
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be Signed-off-by: Ali Caglayan <alizter@gmail.com>
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be Signed-off-by: Ali Caglayan <alizter@gmail.com>
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be Signed-off-by: Ali Caglayan <alizter@gmail.com>
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be Signed-off-by: Ali Caglayan <alizter@gmail.com>
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be Signed-off-by: Ali Caglayan <alizter@gmail.com>
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be Signed-off-by: Ali Caglayan <alizter@gmail.com>
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be Signed-off-by: Ali Caglayan <alizter@gmail.com>
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be Signed-off-by: Ali Caglayan <alizter@gmail.com>
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be Signed-off-by: Ali Caglayan <alizter@gmail.com>
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be Signed-off-by: Ali Caglayan <alizter@gmail.com>
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in ocaml#6049. This continues and finishes an earlier attempt to do someting similar in ocaml#4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be Signed-off-by: Ali Caglayan <alizter@gmail.com>
We omit the need for native to be specified in the coq.theory stanza and instead allow for Dune to automatically detect whether to enable native compilation via the output of `coqc -config` which was exposed in #6049. This continues and finishes an earlier attempt to do someting similar in #4722. Signed-off-by: Ali Caglayan <alizter@gmail.com> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be Signed-off-by: Ali Caglayan <alizter@gmail.com>
This is a continuation of #5967. The difference here is that the extra variables have been removed in a following commit. We now only expose:
Coq configuration variables:
Version numbers for Coq: