[coq] Add support for native-mode compilation. #3210

ejgallego · 2020-02-27T04:51:12Z

We add a (mode ...) field to the (coq.theory ...) stanza that when
set to native will have the Coq compiler to generate and install
"native" objects, that is to say, .cmxs libraries containing an
ML-level version of the corresponding Coq module.

As of today, Coq itself does call the ocamlfind ocaml to compile the
object files, this restriction may be lifted in the future however it
is not easy as tactics do have access to "Just-In-Time" native
compilation too.

The patch itself should have been straightforward except for a big
problem due to the way Coq outputs native targets and the limitations
of Dune.

By default, coqc -native-compute on will generate the OCaml-level
objects files under .coq-native/, and the regular .vo object in
the build dir. This scheme doesn't work well with the restriction than
a rule can only produce targets in the same directory.

To workaround this limitation, we pass a special flag to Coq so
.coq-native is dropped from the output path; at install time we do
set the rules up so indeed the objects will be installed under
.coq-native for compatibility. This means this feature will only
work in Coq >= 8.12.1

Moreover, the non-standard location of native objects defeats Coq's
default native include path, so we must pass the additional
non-standard include paths to coqc.

Note that native compilation is disabled by default in the dev
profile, as to speed up build. Please use the release or a custom
profile if you want to avoid this.

ejgallego · 2020-03-18T23:21:41Z

I think the idea for the code is mostly OK [code needs a bit of cleanup but nothing serious]

However there is quite a hairy question in terms of when to enable the native mode.

Compiling with (mode native) is usually very expensive, for example we don't want to do that when developing Coq except for a very few cases.

The approach taken in the makefiles is actually to generate that information at configure-time. That is to say, if -native-compiler no is passed to configure then the native targets won't be generated.

Unfortunately we cannot do that in dune so easily, as that would mean targets for coqc depend on an autogenerated file. We could disable this when the profile is dev, but actually that would forbid a few useful cases too. I dunno what to do then; need to thing a bit more.

Zimmi48 · 2020-03-19T13:42:28Z

Providing different dev profiles seems reasonable to me.

ejgallego · 2020-03-19T21:27:39Z

Providing different dev profiles seems reasonable to me.

Still there is a bad interaction of profiles with Coq's own configure, in the sense that a profile may have native enabled however configure may disable it; then the native objects will fail to be produced and the rule will fail.

This is indeed a consequence of build rules being dependent on configure parameters; you could argue that this stuff should not be controlled by configured parameters but by the build system but I'm afraid Coq upstream will loudly complain about it.

Zimmi48 · 2020-03-20T10:11:21Z

Well, the plan is to remove configure eventually, isn't it? I agree the situation might be a bit messy in the meantime.

ejgallego · 2020-03-21T00:43:52Z

Well, the plan is to remove configure eventually, isn't it? I agree the situation might be a bit messy in the meantime.

For sure I'd like to reduce configure a lot, but precisely the options about enabling / disabling components of the trusted base may be ones people want still to see in.

I think we can move forward with this using profiles, however there could be some way for users to break the build doing some configure hacks.

Zimmi48 · 2020-03-21T14:16:07Z

If we really reduce configure a lot and manage to make it fully optional, then it could be the task of configure to generate the right profile according to users' wishes.

ejgallego · 2020-09-02T18:56:17Z

This is certainly experimental and needs documentation, tests, and quite a bit of refactoring, but I'm marking the PR ready for review as IMHO it won't change much. I hope to have it fully ready soon.

The model for native and Coq is still quite in flux, but this should work for the current use cases.

rgrinberg · 2020-09-03T21:34:06Z

Loos good to me. Just needs rebase + docs + test and it should be ready to merge. Nice work.

ejgallego · 2020-09-16T16:30:24Z

Loos good to me. Just needs rebase + docs + test and it should be ready to merge. Nice work.

Unfortunately this doesn't fully work in more complex cases due to Coq not liking the local lib outputting native objects in ./ vs installed libs having them in ./.coq_native. Moreover, coqdep is buggy and doesn't reflect the dependency of files on the native modules so adding a rule that would copy the .cmxs to .coq_native won't work unless we amend coqdep output.

Let me see what can I do.

[The way Coq handles include paths for native is very very hacky, see https://github.com/coq/coq/blob/95f78398bbfe32d55dc07e7ef1a4dc61b7b80cfd/vernac/library.ml#L510 ]

Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>

rgrinberg

Alright, this looks ready to merge.

ejgallego · 2020-11-26T00:50:05Z

Alright, this looks ready to merge.

You still couldn't push?

rgrinberg · 2020-11-26T01:01:29Z

I think I managed. I see my commit in that list

Signed-off-by: Rudi Grinberg <[email protected]>

ejgallego · 2020-11-26T20:07:53Z

Thanks a lot @rgrinberg , renamed the function, and added a small tweak to make the native on/off flag fully explicit as this will be more robust for Coq 8.13 . We could handle Coq's configure setting better, but as in 8.14 coqnative will be a different output command it is IMHO not worth it.

This is more robust for Coq 8.13, as the user can specify this option at configure time, which for now we don't really respect. Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>

Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>

ejgallego · 2020-11-26T21:32:08Z

@rgrinberg leaving to you to click the merge button due to the 2 new commits.

Zimmi48

Sorry for noticing these small documentation mistakes only now. The documentation says that the supported Coq language versions are 0.1 and 0.2 and forgets to mention 0.3. The documentation of (mode ...) should probably says that it requires version 0.3.

Zimmi48 · 2020-11-27T09:22:17Z

doc/dune-files.rst

@@ -1668,6 +1669,17 @@ The stanza will build all ``.v`` files on the given directory. The semantics of
  composition with the Coq's standard library is supported, but in
  this case the ``Coq`` prefix will be made available in a qualified
  way. Since Coq's lang version ``0.2``.
+- you can enable the production of Coq's native compiler object files
+  by setting ``<coq_native_mode>`` to ``native``, this will pass
+  ``-native-compiler on`` to Coq and install the corresponding object


Sorry for only noticing this now, but you probably meant yes instead of on.

Both are accepted, right? I can switch to yes/no if you want.

I don't know / am not aware. I said this based on the output of coqtop -help.

Yes they are [see for example the discussion on attributes where people advocated for more liberal parsing, but indeed here we see the documentation problem with that apporach]

I hadn't noticed that the documentation says so

doc/dune-files.rst

ejgallego · 2020-11-27T15:37:38Z

Sorry for noticing these small documentation mistakes only now. The documentation says that the supported Coq language versions are 0.1 and 0.2 and forgets to mention 0.3. The documentation of (mode ...) should probably says that it requires version 0.3.

Thanks a lot for taking the time to review this, I will fix ASAP. Note that the support still remains sketchy, I will add a check soon so if coqnative is present and (coq 0.4) or above is used the mode flag is deprecated, and instead we have the split set of rules.

@mrmr1993

…ne-action-plugin, dune-private-libs and dune-glob (2.8.0) CHANGES: - `dune rules` accepts aliases and other non-path rules (ocaml/dune#4063, @mrmr1993) - Action `(diff reference test_result)` now accept `reference` to be absent and in that case consider that the reference is empty. Then running `dune promote` will create the reference file. (ocaml/dune#3795, @bobot) - Ignore special files (BLK, CHR, FIFO, SOCKET), (ocaml/dune#3570, fixes ocaml/dune#3124, ocaml/dune#3546, @ejgallego) - Experimental: Simplify loading of additional files (data or code) at runtime in programs by introducing specific installation sites. In particular it allow to define plugins to be installed in these sites. (ocaml/dune#3104, ocaml/dune#3794, fixes ocaml/dune#1185, @bobot) - Move all temporary files created by dune to run actions to a single directory and make sure that actions executed by dune also use this directory by setting `TMPDIR` (or `TEMP` on Windows). (ocaml/dune#3691, fixes ocaml/dune#3422, @rgrinberg) - Fix bootstrap script with custom configuration. (ocaml/dune#3757, fixes ocaml/dune#3774, @marsam) - Add the `executable` field to `inline_tests` to customize the compilation flags of the test runner executable (ocaml/dune#3747, fixes ocaml/dune#3679, @lubegasimon) - Add `(enabled_if ...)` to `(copy_files ...)` (ocaml/dune#3756, @nojb) - Make sure Dune cleans up the status line before exiting (ocaml/dune#3767, fixes ocaml/dune#3737, @alan-j-hu) - Add `{gitlab,bitbucket}` as options for defining project sources with `source` stanza `(source (<host> user/repo))` in the `dune-project` file. (ocaml/dune#3813, @rgrinberg) - Fix generation of `META` and `dune-package` files when some targets (byte, native, dynlink) are disabled. Previously, dune would generate all archives for regardless of settings. (ocaml/dune#3829, ocaml/dune#4041, @rgrinberg) - Do not run ocamldep to for single module executables & libraries. The dependency graph for such artifacts is trivial (ocaml/dune#3847, @rgrinberg) - Fix cram tests inside vendored directories not being interpreted correctly. (ocaml/dune#3860, fixes ocaml/dune#3843, @rgrinberg) - Add `package` field to private libraries. This allows such libraries to be installed and to be usable by other public libraries in the same project (ocaml/dune#3655, fixes ocaml/dune#1017, @rgrinberg) - Fix the `%{make}` variable on Windows by only checking for a `gmake` binary on UNIX-like systems as a unrelated `gmake` binary might exist on Windows. (ocaml/dune#3853, @kit-ty-kate) - Fix `$ dune install` modifying the build directory. This made the build directory unusable when `$ sudo dune install` modified permissions. (fix ocaml/dune#3857, @rgrinberg) - Fix handling of aliases given on the command line (using the `@` and `@@` syntax) so as to correctly handle relative paths. (ocaml/dune#3874, fixes ocaml/dune#3850, @nojb) - Allow link time code generation to be used in preprocessing executable. This makes it possible to use the build info module inside the preprocessor. (ocaml/dune#3848, fix ocaml/dune#3848, @rgrinberg) - Correctly call `git ls-tree` so unicode files are not quoted, this fixes problems with `dune subst` in the presence of unicode files. Fixes ocaml/dune#3219 (ocaml/dune#3879, @ejgallego) - `dune subst` now accepts common command-line arguments such as `--debug-backtraces` (ocaml/dune#3878, @ejgallego) - `dune describe` now also includes information about executables in addition to that of libraries. (ocaml/dune#3892, ocaml/dune#3895, @nojb) - instrumentation backends can now receive arguments via `(instrumentation (backend <name> <args>))`. (ocaml/dune#3906, ocaml/dune#3932, @nojb) - Tweak auto-formatting of `dune` files to improve readability. (ocaml/dune#3928, @nojb) - Add a switch argument to opam when context is not default. (ocaml/dune#3951, @tmattio) - Avoid pager when running `$ git diff` (ocaml/dune#3912, @AltGr) - Add `(root_module ..)` field to libraries & executables. This makes it possible to use library dependencies shadowed by local modules (ocaml/dune#3825, @rgrinberg) - Allow `(formatting ...)` field in `(env ...)` stanza to set per-directory formatting specification. (ocaml/dune#3942, @nojb) - [coq] In `coq.theory`, `:standard` for the `flags` field now uses the flags set in `env` profile flags (ocaml/dune#3931 , @ejgallego @rgrinberg) - [coq] Add `-q` flag to `:standard` `coqc` flags , fixes ocaml/dune#3924, (ocaml/dune#3931 , @ejgallego) - Add support for Coq's native compute compilation mode (@ejgallego, ocaml/dune#3210) - Add a `SUFFIX` directive in `.merlin` files for each dialect with no preprocessing, to let merlin know of additional file extensions (ocaml/dune#3977, @vouillon) - Stop promoting `.merlin` files. Write per-stanza Merlin configurations in binary form. Add a new subcommand `dune ocaml-merlin` that Merlin can use to query the configuration files. The `allow_approximate_merlin` option is now useless and deprecated. Dune now conflicts with `merlin < 3.4.0` and `ocaml-lsp-server < 1.3.0` (ocaml/dune#3554, @voodoos) - Configurator: fix a bug introduced in 2.6.0 where the configurator V1 API doesn't work at all when used outside of dune. (ocaml/dune#4046, @aalekseyev) - Fix `libexec` and `libexec-private` variables. In cross-compilation settings, they now point to the file in the host context. (ocaml/dune#4058, fixes ocaml/dune#4057, @TheLortex) - When running `$ dune subst`, use project metadata as a fallback when package metadata is missing. We also generate a warning when `(name ..)` is missing in `dune-project` files to avoid failures in production builds. - Remove support for passing `-nodynlink` for executables. It was bypassed in most cases and not correct in other cases in particular on arm32. (ocaml/dune#4085, fixes ocaml/dune#4069, fixes ocaml/dune#2527, @emillon) - Generate archive rules compatible with 4.12. Dune longer attempt to generate an archive file if it's unnecessary (ocaml/dune#3973, fixes ocaml/dune#3766, @rgrinberg) - Fix generated Merlin configurations when multiple preprocessors are defined for different modules in the same folder. (ocaml/dune#4092, fixes ocaml/dune#2596, ocaml/dune#1212 and ocaml/dune#3409, @voodoos) - Add the option `use_standard_c_and_cxx_flags` to `dune-project` that 1. disables the unconditional use of the `ocamlc_cflags` and `ocamlc_cppflags` from `ocamlc -config` in C compiler calls, these flags will be present in the `:standard` set instead; and 2. enables the detection of the C compiler family and populates the `:standard` set of flags with common default values when building CXX stubs. (ocaml/dune#3875, ocaml/dune#3802, fix ocaml/dune#3718 and ocaml/dune#3528, @voodoos)

Fixes ocaml#4142. Changes introduced in ocaml#3210 meant that Dune became incompatible with Coq < 8.10 ; this was not intentional and it turns out we had Coq Dune users in Coq 8.9 / 8.8. Indeed `(using coq 0.3)` does require Coq >= 8.10, but when `(using coq 0.2)` is set, we should remain compatible with Coq 8.7-8.9. Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>

Fixes #4142. Changes introduced in #3210 meant that Dune became incompatible with Coq < 8.10 ; this was not intentional and it turns out we had Coq Dune users in Coq 8.9 / 8.8. Indeed `(using coq 0.3)` does require Coq >= 8.10, but when `(using coq 0.2)` is set, we should remain compatible with Coq 8.7-8.9. Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>

* Otherwise, with Coq 8.13: #=== ERROR while compiling coq-coqeal.1.0.5 ===================================# # [...] # File "./refinements/multipoly.v", line 1532, characters 0-67: # Warning: Duplicate clear of sz_m' [duplicate-clear,ssr] # File "./refinements/.coq-native/NCoqEAL_refinements_multipoly.native", line 66, characters 14-82: # Error: Unbound module NSsrMultinomials_mpoly # Error: Native compiler exited with status 2 * This fix is temporary: when multinomials will require Coq >= 8.12.1, one could then rely on ocaml/dune#3210, which provides the `(mode native)` stanza. * For details, see also: coq/rfcs#48

* Otherwise, with (coq.8.13.2 + coq-native): #=== ERROR while compiling coq-coqeal.1.0.5 ===================================# # [...] # File "./refinements/multipoly.v", line 1532, characters 0-67: # Warning: Duplicate clear of sz_m' [duplicate-clear,ssr] # File "./refinements/.coq-native/NCoqEAL_refinements_multipoly.native", line 66, characters 14-82: # Error: Unbound module NSsrMultinomials_mpoly # Error: Native compiler exited with status 2 * This fix is temporary: when multinomials will require Coq >= 8.12.1, one could then rely on ocaml/dune#3210, which provides the `(mode native)` stanza. * For details, see also: coq/rfcs#48

ejgallego added the coq label Feb 27, 2020

ejgallego force-pushed the coq+native branch 5 times, most recently from 41f2529 to 6fbd545 Compare February 27, 2020 19:11

ejgallego force-pushed the coq+native branch 2 times, most recently from 5b0407d to 378f99c Compare March 18, 2020 23:18

ejgallego force-pushed the coq+native branch from 378f99c to 62135b1 Compare March 22, 2020 04:05

ejgallego force-pushed the coq+native branch from 62135b1 to 58b6952 Compare April 1, 2020 07:35

ejgallego mentioned this pull request Apr 4, 2020

bignums failing coq/coq-bench#83

Closed

proux01 mentioned this pull request Apr 13, 2020

[dune] [stdlib] Build the standard library natively with Dune. coq/coq#11539

Merged

ejgallego force-pushed the coq+native branch from 58b6952 to 63dac65 Compare May 19, 2020 18:58

ejgallego mentioned this pull request Jun 22, 2020

Dune should not disable native_compute coq/coq#8860

Closed

ejgallego force-pushed the coq+native branch 2 times, most recently from 9d2e2e2 to c9040e4 Compare September 2, 2020 18:03

ejgallego changed the title ~~[wip] [coq] Add support for native-mode compilation.~~ [coq] Add support for native-mode compilation. Sep 2, 2020

ejgallego marked this pull request as ready for review September 2, 2020 18:54

ejgallego force-pushed the coq+native branch from 7d6b1ef to 5a1dafb Compare September 2, 2020 18:59

rgrinberg added this to the 2.8 milestone Sep 3, 2020

ejgallego force-pushed the coq+native branch from 5a1dafb to 933ef6d Compare October 9, 2020 15:43

ejgallego added 2 commits November 26, 2020 00:39

[coq] Don't build native files when profile == dev

c6a80ce

Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>

[coq] Documentation and changes for (mode native)

f688adf

Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>

rgrinberg approved these changes Nov 25, 2020

View reviewed changes

coqc_native_flags: Do not raise exceptions eagerly

fd6a712

Signed-off-by: Rudi Grinberg <[email protected]>

ejgallego force-pushed the coq+native branch from 4022dcc to 7c739fc Compare November 26, 2020 20:06

ejgallego added 2 commits November 26, 2020 21:35

[coq] Be explicit about native mode in command line flags

0337d3e

This is more robust for Coq 8.13, as the user can specify this option at configure time, which for now we don't really respect. Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>

[coq] Renaming function as suggested in review.

454dae6

Signed-off-by: Emilio Jesus Gallego Arias <[email protected]>

ejgallego force-pushed the coq+native branch from 7c739fc to 454dae6 Compare November 26, 2020 20:35

rgrinberg merged commit 181555d into ocaml:master Nov 27, 2020

Zimmi48 reviewed Nov 27, 2020

View reviewed changes

ejgallego deleted the coq+native branch November 27, 2020 15:35

rgrinberg mentioned this pull request Jan 13, 2021

[new release] dune-build-info, dune, dune-configurator, dune-site, dune-action-plugin, dune-private-libs and dune-glob (2.8.0) ocaml/opam-repository#17967

Merged

LasseBlaauwbroek mentioned this pull request Jan 20, 2021

coqc: ondemand: no such file or directory #4142

Closed

ejgallego mentioned this pull request Feb 14, 2021

[coq] Restore compatibility with Coq < 8.10 for coq-lang < 0.3 #4224

Merged

erikmd mentioned this pull request Apr 8, 2021

fix: Use coq_makefile instead of dune, temporarily math-comp/multinomials#41

Closed

liyishuai mentioned this pull request Jun 5, 2022

Update Dune Lysxia/coq-simple-io#55

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[coq] Add support for native-mode compilation. #3210

[coq] Add support for native-mode compilation. #3210

ejgallego commented Feb 27, 2020 •

edited

Loading

ejgallego commented Mar 18, 2020

Zimmi48 commented Mar 19, 2020

ejgallego commented Mar 19, 2020

Zimmi48 commented Mar 20, 2020

ejgallego commented Mar 21, 2020

Zimmi48 commented Mar 21, 2020

ejgallego commented Sep 2, 2020

rgrinberg commented Sep 3, 2020

ejgallego commented Sep 16, 2020 •

edited

Loading

rgrinberg left a comment

ejgallego commented Nov 26, 2020

rgrinberg commented Nov 26, 2020

ejgallego commented Nov 26, 2020

ejgallego commented Nov 26, 2020

Zimmi48 left a comment

Zimmi48 Nov 27, 2020

ejgallego Nov 27, 2020

Zimmi48 Nov 27, 2020

ejgallego Nov 27, 2020

ejgallego commented Nov 27, 2020

[coq] Add support for native-mode compilation. #3210

[coq] Add support for native-mode compilation. #3210

Conversation

ejgallego commented Feb 27, 2020 • edited Loading

ejgallego commented Mar 18, 2020

Zimmi48 commented Mar 19, 2020

ejgallego commented Mar 19, 2020

Zimmi48 commented Mar 20, 2020

ejgallego commented Mar 21, 2020

Zimmi48 commented Mar 21, 2020

ejgallego commented Sep 2, 2020

rgrinberg commented Sep 3, 2020

ejgallego commented Sep 16, 2020 • edited Loading

rgrinberg left a comment

Choose a reason for hiding this comment

ejgallego commented Nov 26, 2020

rgrinberg commented Nov 26, 2020

ejgallego commented Nov 26, 2020

ejgallego commented Nov 26, 2020

Zimmi48 left a comment

Choose a reason for hiding this comment

Zimmi48 Nov 27, 2020

Choose a reason for hiding this comment

ejgallego Nov 27, 2020

Choose a reason for hiding this comment

Zimmi48 Nov 27, 2020

Choose a reason for hiding this comment

ejgallego Nov 27, 2020

Choose a reason for hiding this comment

ejgallego commented Nov 27, 2020

ejgallego commented Feb 27, 2020 •

edited

Loading

ejgallego commented Sep 16, 2020 •

edited

Loading