Create (stdlib) syntax for Coq stanza #6164

LasseBlaauwbroek · 2022-09-27T08:32:24Z

@ejgallego could you make some comments?

src/dune_rules/coq_rules.ml

ejgallego · 2022-09-27T10:41:52Z

This is def going in the good direction ! A test case is needed too.

It could be the case that the logic for this is better handled using the bootstrap logic, we need to modify that too, as when (stdlib no) is set, and a stdlib is in scope, we need to avoid adding it to the list of (implicit) lib deps.

LasseBlaauwbroek · 2022-09-27T13:28:24Z

I tried testing this with Tactician while composed with Coq. But I didn't get very far, even without these new changes and without any kind of -noinit or -boot flag on Dune 3.4.1:

$ dune build user-contrib/Tactician/theories/Ltac1.vo
File "user-contrib/Tactician/theories/dune", line 1, characters 0-168:
1 | (coq.theory
2 |  (name Tactician)
3 |  (package coq-tactician)
4 |  (libraries
5 |    coq-tactician.record-plugin
6 |    coq-tactician.tactics-plugin
7 |    coq-tactician.ssreflect-plugin
8 |  )
9 | )
cannot guess a path for Coq libraries; please use -coqlib option or ensure you have installed the package containing Coq's stdlib (coq-stdlib in OPAM) If you intend to use Coq without a standard library, the -boot -noinit options must be used.

It seems that Dune is trying to build Tactician's library before the prelude is built. I do not remember this issue existing before...

ejgallego · 2022-09-27T13:37:47Z

@LasseBlaauwbroek oh, likely that's because Coq upstream doesn't ship theories/dune anymore, so Dune doesn't see Coq's stdlib. Can you try again and rename theories/dune.disabled in Coq's upstream?

Yes, the whole setup evolution of Coq + Dune is "interesting" to say the very least.

LasseBlaauwbroek · 2022-09-27T13:40:55Z

You mean rename dune.disabled to dune? If I do that, it does indeed compile... What is the story here? Is the disabled dune file expected to become default again?

ejgallego · 2022-09-27T14:11:51Z

You mean rename dune.disabled to dune? If I do that, it does indeed compile... What is the story here? Is the disabled dune file expected to become default again?

Hopefully. The story is that Coq now generates theories/dune as to be able to fully migrate to Dune, as otherwise we were missing a few features such as configure-time native support and a couple other more.

The current state is interim only in order to be able to cleanup all the non-dune infrastructure in Coq. Also, we are blocked in Dune not allowing to include auto-generated dune files, otherwise we could have a much simpler setup with theories/dune including the auto-generated part.

LasseBlaauwbroek · 2022-09-27T14:29:42Z

Another issue

dune build coq-tactician.install
File "user-contrib/Tactician/theories/dune", line 1, characters 0-183:
 1 | (coq.theory
 2 |  (name Tactician)
 3 |  (package coq-tactician)
 4 |  ; (stdlib no)
 5 |  (libraries
 6 |    coq-tactician.record-plugin
 7 |    coq-tactician.tactics-plugin
 8 |    coq-tactician.ssreflect-plugin
 9 |  )
10 | )
*** Error: in file Ltac1/Record.v, could not find META.coq-core.

ejgallego · 2022-09-27T14:39:15Z

Error: in file Ltac1/Record.v, could not find META.coq-core.

This is a known issue, you need to use the hybrid Declare ML Module syntax still.

LasseBlaauwbroek · 2022-09-27T14:45:52Z

Here, you informed that I shouldn't use the hybrid syntax... coq/coq#16510 (comment)

LasseBlaauwbroek · 2022-09-27T15:00:02Z

I'm also trying to write a test, but I cannot even get the existing tests to complete. I'm running make test-coq, it is unclear which Coq version I should use for the tests. All the ones that I've tried have failed the tests in different ways...

ejgallego · 2022-09-27T15:02:03Z

Here, you informed that I shouldn't use the hybrid syntax... coq/coq#16510 (comment)

Unfortunately that only works if you are not composing with the plugin in scope... If the plugin is not installed, you have this problem. Yeah the current state is not the best :/

Maybe you can keep that syntax for now, but issue a dune build _build/install/default/lib/coq-core/META first ?

There are two serious bugs for compositing with Coq >= 8.16 in current dune master, hopefully we can fix them asap.

LasseBlaauwbroek · 2022-09-27T15:21:04Z

Yes that works. But given that there are currently quite a few issues with composition, would it be reasonable to forego integrating this PR with the bootstrap logic? I cannot really test this, because it is unclear to me which issues are part of this PR and which are not...

If you can explain to me how to properly run the make test-coq tests, then I can add a small test for (stdlib no), like you asked.

ejgallego · 2022-09-27T16:41:00Z

If you can explain to me how to properly run the make test-coq tests, then I can add a small test for (stdlib no), like you asked.

That should work out of the box [use the suggested opam switch in Dune's makefile]

Yes that works. But given that there are currently quite a few issues with composition, would it be reasonable to forego integrating this PR with the bootstrap logic?

I think it is a good idea yes that (stdlib no) first works without a composed lib, but you'll need to hook into boot_lib_flags anways.

LasseBlaauwbroek · 2022-09-27T16:57:14Z

That should work out of the box [use the suggested opam switch in Dune's makefile]

Thanks. I missed the dev-switch target.

but you'll need to hook into boot_lib_flags anways.

I don't really know what that means. I don't really understand the full semantics of (boot) nor how you'd like me to modify it.

ejgallego · 2022-09-27T16:58:40Z

I don't really know what that means. I don't really understand the full semantics of (boot) nor how you'd like me to modify it.

I mean that the place that you will have to tweak the flags generation is the function named boot_lib_flags. Once you tweak that function, composition should also work fine.

LasseBlaauwbroek · 2022-09-27T17:19:38Z

Another issue: It appears that dune is not passing the following flags to coqc in a composed build: -I plugins/syntax -I plugins/cc.

LasseBlaauwbroek · 2022-09-27T17:58:10Z

Once you tweak that function, composition should also work fine.

Unfortunately, I don't really know what this 'tweak' should be.

W.r.t. the composed build, I'm now stuck on this error:

$ ../../dune/dune.exe build coq-tactician.install
File "./user-contrib/Tactician/theories/Ltac1/Record.v", line 5, characters 0-42:
Error:
System error: "/home/lasse/Documents/Projects/Tactician/coqdev/coq/_build/install/default/lib/coq-core/plugins/ltac/ltac_plugin.cmxs: No such file or directory"

It seems that plugins are not being properly promoted to the install directory?

ejgallego · 2022-09-27T18:59:13Z

Umm, that last one seems bizarre, but maybe you can try what I posted on the issue:

@LasseBlaauwbroek , Ali and I tried to fix the composition bug in #6165 , it was a bit tricky, but indeed, we added the flag to the buildable as we were going along. I think you can rebase your PR on top of that one, and add the tests, the syntax extension, and the documentation, and let us know how it works.

ejgallego · 2022-09-27T19:03:05Z

I'd suggest first adding a use case, use the one we added in the PR as a base if you want. Once the use case is working fine, you can see how it works on your own setup.

I'd be happy to try the tactician build if you point me out to the right tree.

LasseBlaauwbroek · 2022-09-27T19:16:17Z

Thanks @ejgallego, I'll try out the PR and see if it works.

With regard to writing tests and use cases, I think that we are talking past each other a little bit: I have absolutely no idea what I'm doing...

I do not understand what the intended semantics of (boot) is, neither do I know what 'the bug' related to this is. All I know is that (boot) is used to bootstrap Coq's standard library.
There seem to be so many bugs and issues that I'm have trouble seeing the trees in the forest.
I'm unsure what a test or use-case is supposed to test? Just that the (stdlib no) syntax exists and passes -boot to coqc and coqdep? Something related to (boot)? Something related to composition?

LasseBlaauwbroek · 2022-09-27T19:21:45Z

Here is the tree with some changes to Tactician that I'm currently using to try to make the composable build work: https://github.com/coq-tactician/coq-tactician/tree/no-stdlib-attempt

ejgallego · 2022-09-27T19:42:25Z

3. I'm unsure what a test or use-case is supposed to test? Just that the (stdlib no) syntax exists and passes -boot to coqc and coqdep?

Yes. To merge this we need that test, a changes entry, and a documentation update.

Something related to (boot)? Something related to composition?

That's optional IMHO, but easy to do if you want, start from some of the compose-*boot* tests, and for example verify that building a (stdlib no) library doesn't build the one that has (boot).

By the way, the semantics of (boot) are not documented on purpose, but easy (once the PR fixing them is merged), it just tells dune that the library marked with boot has:

a $path/Init/ directory which is compiled with -boot -noinit
all other libraries implicitly depend on it, and will implicitly load Prelude.vo

Actually both of these features could be modeled with smaller independent features:

for the boot library, we could use per-file flags
we could require the implicit dependency to be made explicit (we will soon)
coqdep could add the missing Prelude.vo deps, however this is a bit harder as it is not backwards compatible.

ejgallego · 2022-09-27T20:09:08Z

Here is the tree with some changes to Tactician that I'm currently using to try to make the composable build work: https://github.com/coq-tactician/coq-tactician/tree/no-stdlib-attempt

Your tree builds fine, but you need to still use the compat syntax, diff:

diff --git a/theories/Ltac1/Record.v b/theories/Ltac1/Record.v
index 0b1158c..1bc407c 100644
--- a/theories/Ltac1/Record.v
+++ b/theories/Ltac1/Record.v
@@ -2,11 +2,11 @@
 Definition private_constant_placeholder (x : Type) := x.
 Register private_constant_placeholder as tactician.private_constant_placeholder.
 
-Declare ML Module "coq-core.plugins.ltac".
-Declare ML Module "coq-core.plugins.firstorder".
-Declare ML Module "coq-core.plugins.extraction".
-Declare ML Module "coq-core.plugins.funind".
-Declare ML Module "coq-tactician.record-plugin".
+Declare ML Module "ltac_plugin:coq-core.plugins.ltac".
+Declare ML Module "firstorder_plugin:coq-core.plugins.firstorder".
+Declare ML Module "extraction_plugin:coq-core.plugins.extraction".
+Declare ML Module "funind_plugin:coq-core.plugins.funind".
+Declare ML Module "tactician_ltac1_record_plugin:coq-tactician.record-plugin".
 Export Set Default Proof Mode "Tactician Ltac1".
 
 Tactician Record Then Decompose.
diff --git a/theories/Ltac1/Tactics.v b/theories/Ltac1/Tactics.v
index 9461a3d..06e809c 100644
--- a/theories/Ltac1/Tactics.v
+++ b/theories/Ltac1/Tactics.v
@@ -1,6 +1,6 @@
 From Tactician Require Export Ltac1.Record.
 
-Declare ML Module "coq-tactician.tactics-plugin".
+Declare ML Module "tactician_ltac1_tactics_plugin:coq-tactician.tactics-plugin".
 
 Tactic Notation (at level 5) "search" "with" "cache" tactic3(t) := fail
   "'search with cache' has been renamed to 'synth with cache'".

LasseBlaauwbroek · 2022-09-27T21:05:26Z

Yes, that does indeed work (I feel stupid now for not thinking about that but the error messages were truly coming from everwhere). Thanks.

LasseBlaauwbroek · 2022-09-27T21:11:06Z

I tried to rebase this on top of #6165, but it looks like you've already integrated the new syntax introduced here?

CHANGES.md

test/blackbox-tests/test-cases/coq/no-stdlib.t/run.t

ejgallego

LGTM modulo maybe a couple of typos below? I think we should squash the commits too.

Also let's add a test where boot is in scope, and we use stdlib={yes,no}

LasseBlaauwbroek · 2022-10-03T15:42:21Z

Squashed and fixed the comments you made.

Alizter · 2022-10-03T16:22:07Z

@LasseBlaauwbroek Can you ./dune.exe fmt to make the linter happy?

LasseBlaauwbroek · 2022-10-03T16:23:36Z

Done.

LasseBlaauwbroek · 2022-10-03T16:37:44Z

I believe that I already addressed that one.

christinerose

suggestions for formatting, typo fixed

CHANGES.md

test/blackbox-tests/test-cases/coq/compose-boot-nostdlib.t/run.t

christinerose · 2022-10-03T20:50:09Z

test/blackbox-tests/test-cases/coq/coqtop-root.t/run.t

@@ -14,5 +14,5 @@ This test is currently broken due to the workspace resolution being faulty #5899
  1 | (coq.theory
  2 |  (name foo))
  Error: 'coq.theory' is available only when coq is enabled in the dune-project


Suggested change

Error: 'coq.theory' is available only when coq is enabled in the dune-project

Error: 'coq.theory' is available only when Coq is enabled in the ``dune-project``

This is automatically generated output.

But also technically correct since it is talking about the coq mode which is enabled in the dune-project file.

Ah! Thanks for clarifying. Perhaps both coq and dune-project in monospace then?

Since it appears in a command line error message, demarking it monospace would waste space.

@christinerose These are Cram (I/O) tests. The test system runs specified commands, and the output of the commands is compared against what is committed here. Hence, you cannot just change this output because then the tests would fail. If you would want to change the wording of the messages, you'd have to do it where the I/O is actually performed.

(As an additional note, I'd say that the required standard of copy-editing in tests is a bit lower than one would expect for, say, documentation.)

Understood. Please feel free to discard anything that's not useful. I was tagged to review, so I did my thing. 😄 .... Do you need me to go back and "approve" it before you can move forward?

No, the PR has already been merged and completed. Thanks for your comments @christinerose.

christinerose · 2022-10-03T20:50:50Z

test/blackbox-tests/test-cases/coq/coqtop-root.t/run.t

@@ -14,5 +14,5 @@ This test is currently broken due to the workspace resolution being faulty #5899
  1 | (coq.theory
  2 |  (name foo))
  Error: 'coq.theory' is available only when coq is enabled in the dune-project
-  file. You must enable it using (using coq 0.5) in your dune-project file.
+  file. You must enable it using (using coq 0.6) in your dune-project file.


Suggested change

file. You must enable it using (using coq 0.6) in your dune-project file.

file. You must enable it using (using ``coq 0.6``) in your ``dune-project`` file.

Autogenerated output.

christinerose · 2022-10-03T20:51:31Z

test/blackbox-tests/test-cases/coq/github3624.t

@@ -16,5 +16,5 @@ that the error message is good when the coq extension is not enabled.
  1 | (coq.theory
  2 |  (name foo))
  Error: 'coq.theory' is available only when coq is enabled in the dune-project


Suggested change

Error: 'coq.theory' is available only when coq is enabled in the dune-project

Error: 'coq.theory' is available only when Coq is enabled in the ``dune-project``

Autogenerated output.

christinerose · 2022-10-03T20:51:45Z

test/blackbox-tests/test-cases/coq/github3624.t

@@ -16,5 +16,5 @@ that the error message is good when the coq extension is not enabled.
  1 | (coq.theory
  2 |  (name foo))
  Error: 'coq.theory' is available only when coq is enabled in the dune-project
-  file. You must enable it using (using coq 0.5) in your dune-project file.
+  file. You must enable it using (using coq 0.6) in your dune-project file.


Suggested change

file. You must enable it using (using coq 0.6) in your dune-project file.

file. You must enable it using (using ``coq 0.6``) in your ``dune-project`` file.

Autogenerated output.

Autogenerated from where? Like by odoc?

This is the command line error message of Dune.

Fixes ocaml#6163 Co-authored-by: Christine Rose <[email protected]> Signed-off-by: Lasse Blaauwbroek <[email protected]>

ejgallego

Great!

LasseBlaauwbroek · 2022-10-04T08:45:54Z

Thanks everyone!

@rgrinberg

…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)

@rgrinberg

…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)

LasseBlaauwbroek force-pushed the stdlib-no branch 3 times, most recently from b56b0e7 to 4fb9afa Compare September 27, 2022 08:39

ejgallego reviewed Sep 27, 2022

View reviewed changes

src/dune_rules/coq_rules.ml Outdated Show resolved Hide resolved

ejgallego self-assigned this Sep 27, 2022

ejgallego mentioned this pull request Sep 27, 2022

[coq] Fix composition of boot library when it has plugins, add field to allow libraries to opt out of stdlib #6165

Merged

Alizter approved these changes Oct 2, 2022

View reviewed changes

ejgallego reviewed Oct 3, 2022

View reviewed changes

CHANGES.md Outdated Show resolved Hide resolved

ejgallego reviewed Oct 3, 2022

View reviewed changes

test/blackbox-tests/test-cases/coq/no-stdlib.t/run.t Outdated Show resolved Hide resolved

ejgallego reviewed Oct 3, 2022

View reviewed changes

LasseBlaauwbroek force-pushed the stdlib-no branch 2 times, most recently from 5868645 to 384a0b8 Compare October 3, 2022 15:40

LasseBlaauwbroek force-pushed the stdlib-no branch from 384a0b8 to 9f30645 Compare October 3, 2022 15:43

Alizter approved these changes Oct 3, 2022

View reviewed changes

LasseBlaauwbroek force-pushed the stdlib-no branch from 9f30645 to 726cc6f Compare October 3, 2022 16:23

LasseBlaauwbroek force-pushed the stdlib-no branch from 726cc6f to 1c02abf Compare October 3, 2022 16:32

christinerose approved these changes Oct 3, 2022

View reviewed changes

LasseBlaauwbroek force-pushed the stdlib-no branch from 3ff580c to 2d574e4 Compare October 3, 2022 21:10

Create (stdlib) syntax for Coq stanza

d45acf6

Fixes ocaml#6163 Co-authored-by: Christine Rose <[email protected]> Signed-off-by: Lasse Blaauwbroek <[email protected]>

LasseBlaauwbroek force-pushed the stdlib-no branch from 2d574e4 to d45acf6 Compare October 4, 2022 04:06

ejgallego approved these changes Oct 4, 2022

View reviewed changes

Merge branch 'main' into stdlib-no

8f089ac

ejgallego merged commit bf25331 into ocaml:main Oct 4, 2022

LasseBlaauwbroek deleted the stdlib-no branch October 4, 2022 08:45

LasseBlaauwbroek restored the stdlib-no branch October 4, 2022 14:19

LasseBlaauwbroek deleted the stdlib-no branch October 4, 2022 14:19

Alizter added the coq label Oct 11, 2022

emillon mentioned this pull request Oct 19, 2022

[new release] xdg, stdune, ordering, ocamlc-loc, fiber, dyn, dune, dune-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) ocaml/opam-repository#22317

Merged

	Error: 'coq.theory' is available only when coq is enabled in the dune-project
	Error: 'coq.theory' is available only when Coq is enabled in the ``dune-project``

	file. You must enable it using (using coq 0.6) in your dune-project file.
	file. You must enable it using (using ``coq 0.6``) in your ``dune-project`` file.

Create (stdlib) syntax for Coq stanza #6164

Create (stdlib) syntax for Coq stanza #6164

Conversation

LasseBlaauwbroek commented Sep 27, 2022

ejgallego commented Sep 27, 2022

LasseBlaauwbroek commented Sep 27, 2022 • edited Loading

ejgallego commented Sep 27, 2022

LasseBlaauwbroek commented Sep 27, 2022

ejgallego commented Sep 27, 2022

LasseBlaauwbroek commented Sep 27, 2022

ejgallego commented Sep 27, 2022

LasseBlaauwbroek commented Sep 27, 2022

LasseBlaauwbroek commented Sep 27, 2022

ejgallego commented Sep 27, 2022

LasseBlaauwbroek commented Sep 27, 2022

ejgallego commented Sep 27, 2022

LasseBlaauwbroek commented Sep 27, 2022

ejgallego commented Sep 27, 2022

LasseBlaauwbroek commented Sep 27, 2022

LasseBlaauwbroek commented Sep 27, 2022 • edited Loading

ejgallego commented Sep 27, 2022

ejgallego commented Sep 27, 2022

LasseBlaauwbroek commented Sep 27, 2022 • edited Loading

LasseBlaauwbroek commented Sep 27, 2022

ejgallego commented Sep 27, 2022

ejgallego commented Sep 27, 2022

LasseBlaauwbroek commented Sep 27, 2022

LasseBlaauwbroek commented Sep 27, 2022

ejgallego left a comment

Choose a reason for hiding this comment

LasseBlaauwbroek commented Oct 3, 2022

Alizter commented Oct 3, 2022 • edited Loading

LasseBlaauwbroek commented Oct 3, 2022

LasseBlaauwbroek commented Oct 3, 2022

christinerose left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Alizter Oct 3, 2022 • edited Loading

Choose a reason for hiding this comment

LasseBlaauwbroek Oct 3, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ejgallego left a comment

Choose a reason for hiding this comment

LasseBlaauwbroek commented Oct 4, 2022

LasseBlaauwbroek commented Sep 27, 2022 •

edited

Loading

LasseBlaauwbroek commented Sep 27, 2022 •

edited

Loading

LasseBlaauwbroek commented Sep 27, 2022 •

edited

Loading

Alizter commented Oct 3, 2022 •

edited

Loading

Alizter Oct 3, 2022 •

edited

Loading

LasseBlaauwbroek Oct 3, 2022 •

edited

Loading