feature(coq): automatic detection of native #6409

Alizter · 2022-11-08T22:03:45Z

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.

cc @proux01 @ejgallego

rgrinberg · 2022-11-08T23:19:20Z

src/dune_rules/coq_rules.ml

+    else if buildable.coq_lang_version < (0, 7) then Memo.return Coq_mode.VoOnly
+    else
+      let* coqc = resolve_program sctx ~dir ~loc "coqc" in
+      let+ config = Coq_config.make ~bin:(Action.Prog.ok_exn coqc) in


Just an fyi, this breaks lazy loading absolutely everywhere where coq stanzas are present. I'm not sure if you care though.

I think we already broke lazy loading since coqc and coqdep were being resolved in the common context in Coq_rules.

Isn't the resolution inside the monad tho?

proux01 · 2022-11-09T17:02:08Z

@Alizter I just tested and it seems to work great. Do we absolutely need to bring a new version 0.7 of the language? It seems to me that if the default value was changed in version 0.3 of the language starting from dune 3.6, we could just make the coq-native package conflict with dune < 3.6 and get the right behavior for any one using any >= 0.3 version of the language. Otherwise, coq-native will only start working when it will become reasonable for users to require dune >= 3.6 in order to use the 0.7 language.

doc/coq.rst

Alizter · 2022-11-10T13:07:13Z

I think version 0.7 is necessary if we want to preserve the behavior with older versions of Coq lang.

doc/coq.rst

ejgallego · 2022-11-10T15:29:01Z

@Alizter I just tested and it seems to work great. Do we absolutely need to bring a new version 0.7 of the language? It seems to me that if the default value was changed in version 0.3 of the language starting from dune 3.6, we could just make the coq-native package conflict with dune < 3.6 and get the right behavior for any one using any >= 0.3 version of the language. Otherwise, coq-native will only start working when it will become reasonable for users to require dune >= 3.6 in order to use the 0.7 language.

I'm not sure I understand the logic here, if we don't guard this with a build language version, then Coq packages would be built differently when dune is upgraded, so IMO it'd be very bad that upgrading dune is not stable.

Indeed, to take advantage of this feature packages need to require Dune >= 3.6, how would it work otherwise?

coq-native is used to configure Coq, so adding a conflict would make actually the whole native setup non-installable?

ejgallego · 2022-11-10T15:30:38Z

src/dune_rules/coq_rules.ml

-  if Profile.is_dev profile then VoOnly else snd buildable.mode
+let select_native_mode ~sctx ~dir (buildable : Coq_stanza.Buildable.t) =
+  match snd buildable.mode with
+  | Some x -> Memo.return x


I think we still want to avoid building native objects in dev mode, it is very expensive and it doesn't make a lot of sense for users.

At the very least we should preserve the previous behavior.

Tho, thinkin about it, native is more a property of the whole workspace / profile setup than of particular stanzas maybe, mmm, not sure.

src/dune_rules/coq_stanza.ml

proux01 · 2022-11-10T15:32:51Z

@ejgallego adding in coq-native a conflict with dune < 3.6 would make coq-native "require" dune >= 3.6.

Anyway, we decided against that with Ali, so please disregard my comment.

proux01 · 2022-11-10T15:40:33Z

Maybe a stupid question: is it possible to disactivate native only for a single file?

ejgallego · 2022-11-10T15:48:39Z

@ejgallego adding in coq-native a conflict with dune < 3.6 would make coq-native "require" dune >= 3.6.

Ahh sorry, indeed, that would be an option, tho indeed pretty disruptive; IMHO experience shows that it is better to try to have broad support of versions combos, at least for now. We can do something like that when we reach (lang dune 1.0) tho, so indeed we are convinced the setup is more stable.

Maybe a stupid question: is it possible to disactivate native only for a single file?

That's not stupid at all! The current situation is no; what we did before was to disable native when in dev profile.

But we can add support for it.

ejgallego · 2022-11-11T17:03:22Z

@Alizter , the problem here comes because the failing test is declared with (lang coq 0.2) , which set its native mode to Legacy.

This passes no arguments to coqc, in particular, it doesn't disable native properly, so in the re-run the native object files will be missing as they are cleaned by Dune.

It seems main again has a bug in this regard, as it should be failing, but for some reason the test runs with VoOnly.

But I'd propose we remove Coq 0.1 and 0.2 and support for 8.10 ; let's deprecate them first.

ejgallego · 2022-11-11T17:05:29Z

See the relevant log for that test in main:

(cd _build/default && /home/egallego/external/dune/_opam/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -R a a a/a.v)

vs in this PR

(cd _build/default && /home/egallego/external/dune/_opam/bin/coqc -q -R a a a/a.v)

… 0.2 Since ocaml#6409 we automatically infer rules for coq-native, and in general this requires at least Coq 8.10 due to the need of command-line option flags added in that version for native. The recommended path for most projects is just to upgrade their dune file and Coq version file. Coq 8.10 will likely be the base we support in `(lang coq 1.0)`.

… 0.2 Since ocaml#6409 we automatically infer rules for coq-native, and in general this requires at least Coq 8.10 due to the need of command-line option flags added in that version for native. The recommended path for most projects is just to upgrade their dune file and Coq version file. Coq 8.10 will likely be the base we support in `(lang coq 1.0)`. Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>

ejgallego · 2022-11-14T14:33:18Z

test/blackbox-tests/test-cases/coq/coqdep-on-rebuild.t/dune-project


-(using coq 0.2)
+(using coq 0.7)


Wouldn't it be better for this to correspond to the version the test was introduced?

I don't see the point.

The point would be consistency with the common practice we do, the test doesn't require coq lang 0.7 so in this sense the new constraint is an over-requirement.

But 0.2 brings out the legacy native mode which is broken. I guess the next one to choose would be 0.3, but why not just use 0.7?

ejgallego

LGTM, however:

previous behavior on profile dev should be preserved if lang \lt 0.7
this change should be better documented in the lang changelog
you could additionally deprecate (mode native) if lang == 0.7

doc/coq.rst

CHANGES.md

ejgallego · 2022-11-14T20:46:25Z

doc/coq.rst

+  When developing with native, you may want the compilation to be faster. You
+  may add ``(mode vo)`` to your stanza to override the native mode and only
+  compile ``vo`` files. Previous versions of Dune before 3.6 would disable the
+  native rules depending on whether or not the ``dev`` profile was selected.


Umm, this seems a bit bizarre, certainly is not standard dune practice to have to edit an stanza when developing.

I would just state that (mode vo) disables native compilation even if the configure option is set.

We already have that (mode) overrides the configure option. Perhaps I should just mention using a native opam switch or something. Though, I am not certain how this works so I will just remove it all together and leave it to a future doc improvement.

doc/coq.rst

ejgallego

LGTM modulo tweaks in the docs that could be IMHO useful.

Alizter · 2022-11-15T07:56:14Z

Actually I think I won't deprecate mode just yet since we may want to add split native compilation. In fact, I have a patch doing just that I can polish up.

Alizter · 2022-11-15T13:57:11Z

OK I found a way to deprecate only (mode native).

Currently waiting for 0.7 Coq lang.

ejgallego · 2022-11-15T15:22:08Z

Actually I think I won't deprecate mode just yet since we may want to add split native compilation. In fact, I have a patch doing just that I can polish up.

Are you aware of the 2 open PRs to do that and the issues regarding the split setup?

Alizter · 2022-11-15T16:02:48Z

@ejgallego Yeah we can discuss it later.

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 <[email protected]> ps-id: cc90289d-3063-4b5c-a76e-987bd9f250be Signed-off-by: Ali Caglayan <[email protected]>

Alizter · 2022-11-15T16:57:28Z

@ejgallego That should have addressed all your comments.

@rgrinberg

…, dune-rpc, dune-rpc-lwt, dune-private-libs, dune-glob, dune-configurator, dune-build-info, dune-action-plugin and chrome-trace (3.7.0~alpha1) CHANGES: - Fix parsing of OCaml errors that contain code excerpts with `...` in them. (ocaml/dune#7008, @rgrinberg) - Pre-emptively clear screen in watch mode (ocaml/dune#6987, fixes ocaml/dune#6884, @rgrinberg) - Fix cross compilation configuration when a context with targets is itself a host of another context (ocaml/dune#6958, fixes ocaml/dune#6843, @rgrinberg) - Fix parsing of the `<=` operator in *blang* expressions of `dune` files. Previously, the operator would be interpreted as `,`. (ocaml/dune#6928, @tatchi) - Fix `--trace-file` output. Dune now emits a single *complete* event for every executed process. Unterminated *async* events are no longer written. (ocaml/dune#6892, @rgrinberg) - Fix preprocessing with `staged_pps` (ocaml/dune#6748, fixes ocaml/dune#6644, @rgrinberg) - Use colored output with MDX when Dune colors are enabled. (ocaml/dune#6462, @MisterDA) - Make `dune describe workspace` return consistent dependencies for executables and for libraries. By default, compile-time dependencies towards PPX-rewriters are from now not taken into account (but runtime dependencies always are). Compile-time dependencies towards PPX-rewriters can be taken into account by providing the `--with-pps` flag. (ocaml/dune#6727, fixes ocaml/dune#6486, @esope) - Print missing newline after `$ dune exec`. (ocaml/dune#6821, fixes ocaml/dune#6700, @rgrinberg, @Alizter) - Fix binary corruption when installing or promoting in parallel (ocaml/dune#6669, fixes ocaml/dune#6668, @edwintorok) - Use colored output with GCC and Clang when compiling C stubs. The flag `-fdiagnostics-color=always` is added to the `:standard` set of flags. (ocaml/dune#4083, @MisterDA) - Fix the parsing of decimal and hexadecimal escape literals in `dune`, `dune-package`, and other dune s-expression based files (ocaml/dune#6710, @shym) - Report an error if `dune init ...` would create a "dune" file in a location which already contains a "dune" directory (ocaml/dune#6705, @gridbugs) - Fix the parsing of alerts. They will now show up in diagnostics correctly. (ocaml/dune#6678, @rginberg) - Fix the compilation of modules generated at link time when `implicit_transitive_deps` is enabled (ocaml/dune#6642, @rgrinberg) - Allow `$ dune utop` to load libraries defined in data only directories defined using `(subdir ..)` (ocaml/dune#6631, @rgrinberg) - Format dune files when they are named `dune-file`. This occurs when we enable the alternative file names project option. (ocaml/dune#6566, @rgrinberg) - Move `$ dune ocaml-merlin -dump-config=$dir` to `$ dune ocaml merlin dump-config $dir`. (ocaml/dune#6547, @rgrinberg) - Allow compilation rules to be impacted by `(env ..)` stanzas that modify the environment or set binaries. (ocaml/dune#6527, @rgrinberg) - Coq native mode is now automatically detected by Dune starting with Coq lang 0.7. `(mode native)` has been deprecated in favour of detection from the configuration of Coq. (ocaml/dune#6409, @Alizter) - Print "Leaving Directory" whenever "Entering Directory" is printed. (ocaml/dune#6149, fixes ocaml/dune#138, @cpitclaudel, @rgrinberg) - Allow `$ dune ocaml dump-dot-merlin` to run in watch mode. Also this command shouldn't print "Entering Directory" mesages. (ocaml/dune#6497, @rgrinberg) - `dune clean` should no longer fail under Windows due to the inability to remove the `.lock` file. Also, bring the implementation of the global lock under Windows closer to that of Unix. (ocaml/dune#6523, @nojb) - Remove "Entering Directory" messages for `$ dune install`. (ocaml/dune#6513, @rgrinberg) - Stop passing `-q` flag in `dune coq top`, which allows for `.coqrc` to be loaded. (ocaml/dune#6848, fixes ocaml/dune#6847, @Alizter) - Fix missing dependencies when detecting the kind of C compiler we're using (ocaml/dune#6610, fixes ocaml/dune#6415, @emillon) - Allow `(include_subdirs qualified)` for OCaml projects. (ocaml/dune#6594, fixes ocaml/dune#1084, @rgrinberg) - Accurately determine merlin configuration for all sources selected with `copy#` and `copy_files#`. The old heuristic of looking for a module in parent directories is removed (ocaml/dune#6594, @rgrinberg) - Fix inline tests with *js_of_ocaml* and whole program compilation mode enabled (ocaml/dune#6645, @hhugo) - Fix *js_of_ocaml* separate compilation rules when `--enable=effects` ,`--enable=use-js-string` or `--toplevel` is used. (ocaml/dune#6714, ocaml/dune#6828, ocaml/dune#6920, @hhugo) - Fix *js_of_ocaml* separate compilation in presence of linkall (ocaml/dune#6832, ocaml/dune#6916, @hhugo) - Remove spurious build dir created when running `dune init proj ...` (ocaml/dune#6707, fixes ocaml/dune#5429, @gridbugs) - Allow `--sandbox` to affect `ocamldep` invocations. Previously, they were wrongly marked as incompatible (ocaml/dune#6749, @rgrinberg) - Validate the command line arguments for `$ dune ocaml top-module`. This command requires one positional argument (ocaml/dune#6796, fixes ocaml/dune#6793, @rgrinberg) - Add a `dune cache size` command for displaying the size of the cache (ocaml/dune#6638, @Alizter) - Add 4.14.0 MSVC to CI (ocaml/dune#6917, @jonahbeckford) - Fix dependency cycle when installing files to the bin section with `glob_files` (ocaml/dune#6764, fixes ocaml/dune#6708, @gridbugs) - Handle "Too many links" errors when using Dune cache on Windows (ocaml/dune#6993, @nojb)

@gridbugs

…, dune-rpc, dune-rpc-lwt, dune-private-libs, dune-glob, dune-configurator, dune-build-info, dune-action-plugin and chrome-trace (3.7.0) CHANGES: - Allow running `$ dune exec` in watch mode (with the `-w` flag). In watch mode, `$ dune exec` the executed binary whenever it is recompiled. (ocaml/dune#6966, @gridbugs) - `coqdep` is now called once per theory, instead of one time per Coq file. This should significantly speed up some builds, as `coqdep` startup time is often heavy (ocaml/dune#7048, @Alizter, @ejgallego) - Add `map_workspace_root` dune-project stanza to allow disabling of mapping of workspace root to `/workspace_root`. (ocaml/dune#6988, fixes ocaml/dune#6929, @richardlford) - Fix handling of support files generated by odoc. (ocaml/dune#6913, @jonludlam) - Fix parsing of OCaml errors that contain code excerpts with `...` in them. (ocaml/dune#7008, @rgrinberg) - Pre-emptively clear screen in watch mode (ocaml/dune#6987, fixes ocaml/dune#6884, @rgrinberg) - Fix cross compilation configuration when a context with targets is itself a host of another context (ocaml/dune#6958, fixes ocaml/dune#6843, @rgrinberg) - Fix parsing of the `<=` operator in *blang* expressions of `dune` files. Previously, the operator would be interpreted as `<`. (ocaml/dune#6928, @tatchi) - Fix `--trace-file` output. Dune now emits a single *complete* event for every executed process. Unterminated *async* events are no longer written. (ocaml/dune#6892, @rgrinberg) - Fix preprocessing with `staged_pps` (ocaml/dune#6748, fixes ocaml/dune#6644, @rgrinberg) - Use colored output with MDX when Dune colors are enabled. (ocaml/dune#6462, @MisterDA) - Make `dune describe workspace` return consistent dependencies for executables and for libraries. By default, compile-time dependencies towards PPX-rewriters are from now not taken into account (but runtime dependencies always are). Compile-time dependencies towards PPX-rewriters can be taken into account by providing the `--with-pps` flag. (ocaml/dune#6727, fixes ocaml/dune#6486, @esope) - Print missing newline after `$ dune exec`. (ocaml/dune#6821, fixes ocaml/dune#6700, @rgrinberg, @Alizter) - Fix binary corruption when installing or promoting in parallel (ocaml/dune#6669, fixes ocaml/dune#6668, @edwintorok) - Use colored output with GCC and Clang when compiling C stubs. The flag `-fdiagnostics-color=always` is added to the `:standard` set of flags. (ocaml/dune#4083, @MisterDA) - Fix the parsing of decimal and hexadecimal escape literals in `dune`, `dune-package`, and other dune s-expression based files (ocaml/dune#6710, @shym) - Report an error if `dune init ...` would create a "dune" file in a location which already contains a "dune" directory (ocaml/dune#6705, @gridbugs) - Fix the parsing of alerts. They will now show up in diagnostics correctly. (ocaml/dune#6678, @rginberg) - Fix the compilation of modules generated at link time when `implicit_transitive_deps` is enabled (ocaml/dune#6642, @rgrinberg) - Allow `$ dune utop` to load libraries defined in data only directories defined using `(subdir ..)` (ocaml/dune#6631, @rgrinberg) - Format dune files when they are named `dune-file`. This occurs when we enable the alternative file names project option. (ocaml/dune#6566, @rgrinberg) - Move `$ dune ocaml-merlin -dump-config=$dir` to `$ dune ocaml merlin dump-config $dir`. (ocaml/dune#6547, @rgrinberg) - Allow compilation rules to be impacted by `(env ..)` stanzas that modify the environment or set binaries. (ocaml/dune#6527, @rgrinberg) - Coq native mode is now automatically detected by Dune starting with Coq lang 0.7. `(mode native)` has been deprecated in favour of detection from the configuration of Coq. (ocaml/dune#6409, @Alizter) - Print "Leaving Directory" whenever "Entering Directory" is printed. (ocaml/dune#6419, fixes ocaml/dune#138, @cpitclaudel, @rgrinberg) - Allow `$ dune ocaml dump-dot-merlin` to run in watch mode. Also this command shouldn't print "Entering Directory" mesages. (ocaml/dune#6497, @rgrinberg) - `dune clean` should no longer fail under Windows due to the inability to remove the `.lock` file. Also, bring the implementation of the global lock under Windows closer to that of Unix. (ocaml/dune#6523, @nojb) - Remove "Entering Directory" messages for `$ dune install`. (ocaml/dune#6513, @rgrinberg) - Stop passing `-q` flag in `dune coq top`, which allows for `.coqrc` to be loaded. (ocaml/dune#6848, fixes ocaml/dune#6847, @Alizter) - Fix missing dependencies when detecting the kind of C compiler we're using (ocaml/dune#6610, fixes ocaml/dune#6415, @emillon) - Allow `(include_subdirs qualified)` for OCaml projects. (ocaml/dune#6594, fixes ocaml/dune#1084, @rgrinberg) - Accurately determine merlin configuration for all sources selected with `copy#` and `copy_files#`. The old heuristic of looking for a module in parent directories is removed (ocaml/dune#6594, @rgrinberg) - Fix inline tests with *js_of_ocaml* and whole program compilation mode enabled (ocaml/dune#6645, @hhugo) - Fix *js_of_ocaml* separate compilation rules when `--enable=effects` ,`--enable=use-js-string` or `--toplevel` is used. (ocaml/dune#6714, ocaml/dune#6828, ocaml/dune#6920, @hhugo) - Fix *js_of_ocaml* separate compilation in presence of linkall (ocaml/dune#6832, ocaml/dune#6916, @hhugo) - Remove spurious build dir created when running `dune init proj ...` (ocaml/dune#6707, fixes ocaml/dune#5429, @gridbugs) - Allow `--sandbox` to affect `ocamldep` invocations. Previously, they were wrongly marked as incompatible (ocaml/dune#6749, @rgrinberg) - Validate the command line arguments for `$ dune ocaml top-module`. This command requires one positional argument (ocaml/dune#6796, fixes ocaml/dune#6793, @rgrinberg) - Add a `dune cache size` command for displaying the size of the cache (ocaml/dune#6638, @Alizter) - Fix dependency cycle when installing files to the bin section with `glob_files` (ocaml/dune#6764, fixes ocaml/dune#6708, @gridbugs) - Handle "Too many links" errors when using Dune cache on Windows (ocaml/dune#6993, @nojb) - Allow the `cinaps` stanza to set a custom alias. By default, if the alias is not set then the cinaps actions will be attached to both `@cinaps` and `@runtest` (ocaml/dune#6991, @rgrinberg) - Add `(using ctypes 0.3)`. When used, paths in `(ctypes)` are interpreted relative to where the stanza is defined. (ocaml/dune#6883, fixes ocaml/dune#5325, @emillon) - Auto-detect `dune-workspace` files as `dune` files in Emacs (ocaml/dune#7061, @ilankri) - Add native support for polling mode on Windows (ocaml/dune#7010, @yams-yams, @nojb)

Since ocaml#6409 we automatically infer rules for coq-native, and in general this requires at least Coq 8.10 due to the need of command-line option flags added in that version for native. Also, since ocaml#7047 and `(coq lang 0.8)` we detect installed theories, correcting a longstanding problem, we require all users to migrate. The recommended path for most projects is just to upgrade their dune file and Coq version file. Coq 8.10 will likely be the base we support in `(lang coq 1.0)`. Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>

Alizter added the coq label Nov 8, 2022

Alizter added this to the 3.6.0 milestone Nov 8, 2022

Alizter requested a review from christinerose as a code owner November 8, 2022 22:03

rgrinberg reviewed Nov 8, 2022

View reviewed changes

Alizter force-pushed the ps/rr/feature_coq___automatic_detection_of_native branch from afcd98c to f8a630a Compare November 8, 2022 23:45

proux01 reviewed Nov 9, 2022

View reviewed changes

doc/coq.rst Outdated Show resolved Hide resolved

christinerose approved these changes Nov 9, 2022

View reviewed changes

ejgallego self-assigned this Nov 9, 2022

Alizter force-pushed the ps/rr/feature_coq___automatic_detection_of_native branch 2 times, most recently from 7c8341b to d006388 Compare November 10, 2022 13:06

Alizter force-pushed the ps/rr/feature_coq___automatic_detection_of_native branch 3 times, most recently from 0ff0599 to 6a32cf5 Compare November 10, 2022 13:58

proux01 reviewed Nov 10, 2022

View reviewed changes

doc/coq.rst Outdated Show resolved Hide resolved

Alizter force-pushed the ps/rr/feature_coq___automatic_detection_of_native branch from 6a32cf5 to b9ac4fc Compare November 10, 2022 14:54

ejgallego reviewed Nov 10, 2022

View reviewed changes

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

Alizter force-pushed the ps/rr/feature_coq___automatic_detection_of_native branch from b9ac4fc to 821b983 Compare November 10, 2022 23:19

ejgallego mentioned this pull request Nov 11, 2022

[coq] Remove Coq build languages 0.1 to 0.7 #6445

Draft

Alizter force-pushed the ps/rr/feature_coq___automatic_detection_of_native branch from 821b983 to 09a692b Compare November 12, 2022 13:46

Alizter requested a review from ejgallego November 14, 2022 01:33

emillon modified the milestones: 3.6.0, 3.7.0 Nov 14, 2022

ejgallego reviewed Nov 14, 2022

View reviewed changes

Alizter force-pushed the ps/rr/feature_coq___automatic_detection_of_native branch from 0ebcf7b to fbac626 Compare November 14, 2022 20:27

ejgallego reviewed Nov 14, 2022

View reviewed changes

doc/coq.rst Show resolved Hide resolved

ejgallego reviewed Nov 14, 2022

View reviewed changes

CHANGES.md Outdated Show resolved Hide resolved

ejgallego reviewed Nov 14, 2022

View reviewed changes

doc/coq.rst Outdated Show resolved Hide resolved

ejgallego approved these changes Nov 14, 2022

View reviewed changes

Alizter force-pushed the ps/rr/feature_coq___automatic_detection_of_native branch 2 times, most recently from 0603a8a to 029007a Compare November 15, 2022 16:53

Alizter force-pushed the ps/rr/feature_coq___automatic_detection_of_native branch from 029007a to 4f9d811 Compare November 15, 2022 16:55

Alizter merged commit 6305e45 into ocaml:main Nov 15, 2022

Alizter deleted the ps/rr/feature_coq___automatic_detection_of_native branch November 15, 2022 17:17

emillon mentioned this pull request Feb 6, 2023

[new release] xdg, stdune, ordering, ocamlc-loc, 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.7.0~alpha1) ocaml/opam-repository#23248

Closed

Alizter mentioned this pull request Feb 12, 2023

[coq] Improve support for Coq's native compiler #5831

Closed

emillon mentioned this pull request Feb 17, 2023

[new release] xdg, stdune, ordering, ocamlc-loc, 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.7.0) ocaml/opam-repository#23349

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feature(coq): automatic detection of native #6409

feature(coq): automatic detection of native #6409

Alizter commented Nov 8, 2022

rgrinberg Nov 8, 2022

Alizter Nov 10, 2022

ejgallego Nov 10, 2022

proux01 commented Nov 9, 2022

Alizter commented Nov 10, 2022

ejgallego commented Nov 10, 2022

ejgallego Nov 10, 2022

ejgallego Nov 10, 2022

proux01 commented Nov 10, 2022

proux01 commented Nov 10, 2022

ejgallego commented Nov 10, 2022

ejgallego commented Nov 11, 2022

ejgallego commented Nov 11, 2022

ejgallego Nov 14, 2022

Alizter Nov 14, 2022

ejgallego Nov 14, 2022

Alizter Nov 14, 2022

ejgallego left a comment

ejgallego Nov 14, 2022

Alizter Nov 15, 2022

ejgallego left a comment

Alizter commented Nov 15, 2022

Alizter commented Nov 15, 2022 •

edited

Loading

ejgallego commented Nov 15, 2022

Alizter commented Nov 15, 2022

Alizter commented Nov 15, 2022

feature(coq): automatic detection of native #6409

feature(coq): automatic detection of native #6409

Conversation

Alizter commented Nov 8, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

proux01 commented Nov 9, 2022

Alizter commented Nov 10, 2022

ejgallego commented Nov 10, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

proux01 commented Nov 10, 2022

proux01 commented Nov 10, 2022

ejgallego commented Nov 10, 2022

ejgallego commented Nov 11, 2022

ejgallego commented Nov 11, 2022

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

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

Alizter commented Nov 15, 2022

Alizter commented Nov 15, 2022 • edited Loading

ejgallego commented Nov 15, 2022

Alizter commented Nov 15, 2022

Alizter commented Nov 15, 2022

Alizter commented Nov 15, 2022 •

edited

Loading