fix: Use coq_makefile instead of dune, temporarily

[erikmd]

Dear Multinomials maintainers — Cc @strub @CohenCyril,

• I've recently attempted to migrate my opam switches to Coq 8.13, but CoqEAL doesn't compile out-of-the-box because of the current build system of coq-multinomials which does not install the required .coq-native/* files.
• I know this may seem orthogonal to the role of the multinomials library, but it happens all transitive dependencies of a given library (such as CoqEAL or ValidSDP) need to install these additional files for the build to be successful;
• As mentioned in the CEP 48, the current best solution to achieve this just amounts to using coq_makefile.

Hence this PR (using coq_makefile instead of dune for the time being).

Commit details

fix: Use coq_makefile instead of dune, temporarily

• 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 [coq] Add support for native-mode compilation. ocaml/dune#3210, which provides the (mode native) stanza.

• For details, see also: CEP for packaging coq-native coq/rfcs#48

If the content of my PR looks good to you, It'd be awesome to have a 1.5.5-or-so point release :-)

[strub]

Then, let's require Coq >= 8.12.1

[erikmd]

OK; I'll prepare an alternative, smaller pull request ASAP then.

[ejgallego]

Sorry I just saw this, a couple of comments:

I've recently attempted to migrate my opam switches to Coq 8.13, but CoqEAL doesn't compile out-of-the-box because of the current build system of coq-multinomials which does not install the required .coq-native/* files.

Actually you can add (mode native) to the dune file and that should work, but that should be added conditionally; I guess using a small configure hack that updates the dune file would work.

For native, dune 3.0 will both support separate compilation and querying configure and setting the build rules dynamically [due to a refactoring of Dune's codebase as to handle dynamic rules better], so that should remove the need of any hack finally.

[proux01]

What happens on (mode native) when Coq has been built without support of native compilation? If I remember correctly, this is just a warning, maybe we could live with it (until this gets fixed with dune 3.0).

[ejgallego]

What happens on (mode native) when Coq has been built without support of native compilation? If I remember correctly, this is just a warning, maybe we could live with it (until this gets fixed with dune 3.0).

Indeed, it should not be present in the dune file; so what I propose is to have a small configure step that does "if coqc -config has native, then insert (mode native) in the dune file.

It is hacky, specially in composed builds, I know.

[erikmd]

Hi all, thanks for your comments!

OK; I'll prepare an alternative, smaller pull request ASAP then.

Sorry, this took quite some time (§). Anyway I'm working tonight to propose a better PR (using dune) that will subsumes this PR.
And I'll close #41 as soon as the other PR is opened.

[(§) FTR a blocking component for me to come up with another PR and test it easily, was the version of dune provided in Docker-Coq, which used to be too old… but the dune version was bumped to 2.9.1 as part of the last rebuild of all Docker-Coq images.]

[erikmd]

BTW @ejgallego

add (mode native) to the dune file and that should work, but that should be added conditionally

do you believe that one such conditional add could be done in dune syntax itself?

otherwise, no worries, I could propose a very simple bash configure script:

• checking that coqc -config | grep 'COQ_NATIVE_COMPILER_DEFAULT=yes' holds
• or that coqc -version yields a version ≥ 8.12.1 & < 8.13 (ref.)

[ejgallego]

do you believe that one such conditional add could be done in dune syntax itself?

Indeed, but will require Dune 3.0 :/

Not sure if the OCaml Syntax mode could help you here, but let me expand a bit more what the problem is.

Build systems make different tradeoffs between what's static and what dynamic. The more static stuff you have, the better you can schedule, (c.f. for example [1])

In Dune 2.x series, build rules are not allowed to depend on the result of other build rules; at least, not in an straightforward way; because actually, Dune has always supported dynamic dependencies [a rule depends on the output of coqdep for example.

This distinction was artificial indeed, and removed in Dune 3.0.

Why dune 2.0 doesn't implement the rule "call coqc, then get the version / flags, and setup the env correctly"? Indeed, because of that artificial restriction on the API. We could do that, however, Dune will complain in the case coq is vendored, thus, it has to build coqc itself to determine the library build rules.

As this is not a problem in Dune 3.0, we have two situations:

• dune 3.0: Dune will be able to query coqc for capabilities and setup the rule correctly
• dune 2.x: Dune can't query coqc in a sound way, thus the choice has to be external.

Thus, in the 2.x case, I'd recommend having indeed a small configure script, that all it does is to copy dune.in to dune and fill the (mode native) depending on the output of coqc. That's ugly, but provides a clear conversion path later on, as you will be able to write stuff like this in Dune 3.0:

(rule
  (targets dune)
  (deps dune.in)
  (action (run ./configure)))

[1] https://www.cambridge.org/core/journals/journal-of-functional-programming/article/build-systems-a-la-carte-theory-and-practice/097CE52C750E69BD16B78C318754C7A4

[erikmd]

Hi @ejgallego, OK, thanks a lot for your detailed comment!

Indeed, let's stick to a small configure script for now.

For completeness, yet another alternative could be to just check directly in *.opam syntax if the coq-native opam package is installed − {coq-native:installed} − then tweak the dune configuration accordingly;
but admittedly, this simpler solution would be too package-manager-centric (opam-only), so I agree that a more generic solution directly using dune and a small configure script is better.

[ejgallego]

Indeed @erikmd , thanks.

I think indeed it makes sense to expose the config variables as coqc -config spills them, similarly to what is done with ocaml, for example you have %{ocaml:version} etc... as dune variables so you can do nice stuff such as compat libraries etc... more easily.

I hope to implement %{coq:version} soon in Dune's master [didn't because I always build Coq vendored, so then it was totally broken for me], but you gave me the idea to also expose %{coq:native-compiler} and a few others, cc ocaml/dune#1998

[erikmd]

• Closing this PR now, as it's subsumed by Add coq-native support (if available) as per CEP 48 #45