problem installing coqeal with opam

[thery]

There seems to be a checksum problem with coqeal 1.0.5

% opam install coq-coqeal
The following actions will be performed:
  - install coq-mathcomp-multinomials 1.5.4         [required by coq-coqeal]
  - install coq-paramcoq              1.1.2+coq8.13 [required by coq-coqeal]
  - install coq-coqeal                1.0.5
===== 3 to install =====
Do you want to continue? [Y/n] y

<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[coq-paramcoq.1.1.2+coq8.13] downloaded from https://github.com/coq-community/paramcoq/archive/v1.1.2+coq8.13.tar.gz
[coq-mathcomp-multinomials.1.5.4] downloaded from https://github.com/math-comp/multinomials/archive/1.5.4.tar.gz
[ERROR] The sources of the following couldn't be obtained, aborting:
          - coq-coqeal.1.0.5: Bad checksum

[proux01]

@thery The checksum seems correct here. Could you try an opam update (the most recent version of Coqeal is 1.0.6 so if you did not explicitly requested installation of 1.0.5, your opam might be outdated and not aware of the move of the github project to coq-community which might explain the issue).

[thery]

it works, thanks

[proux01]

Nice, I'm closing this then.

[thery]

ok I've tried to reinstall coqeal with coq_native and it fails

% opam install coq-coqeal
The following actions will be performed:
  ∗ install coq-coqeal 1.0.6

<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[coq-coqeal.1.0.6] found in cache

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[ERROR] The compilation of coq-coqeal failed at "/home/thery/opam-coq.8.13.2/opam-init/hooks/sandbox.sh build make -j3".

#=== ERROR while compiling coq-coqeal.1.0.6 ===================================#
# context     2.0.8 | linux/x86_64 | ocaml-base-compiler.4.12.0 | https://coq.inria.fr/opam/released#2021-10-04 20:20
# path        /home/thery/opam-coq.8.13.2/default/.opam-switch/build/coq-coqeal.1.0.6
# command     /home/thery/opam-coq.8.13.2/opam-init/hooks/sandbox.sh build make -j3
# exit-code   2
# env-file    /home/thery/opam-coq.8.13.2/log/coq-coqeal-93741-d2c37b.env
# output-file /home/thery/opam-coq.8.13.2/log/coq-coqeal-93741-d2c37b.out
### output ###
# [...]
# File "./refinements/.coq-native/NCoqEAL_refinements_multipoly.native", line 66, characters 14-82:
# 66 |   (Obj.magic (NSsrMultinomials_mpoly.Construct_NSsrMultinomials_mpoly_multinom_0_1 (
#                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
# Error: Unbound module NSsrMultinomials_mpoly
# Error: Native compiler exited with status 2
# 
# make[2]: *** [Makefile.coq:719: refinements/multipoly.vo] Error 1
# make[2]: *** Waiting for unfinished jobs....
# Finished transaction in 2.463 secs (2.456u,0.001s) (successful)
# make[1]: *** [Makefile.coq:343: all] Error 2
# make[1]: Leaving directory '/home/thery/opam-coq.8.13.2/default/.opam-switch/build/coq-coqeal.1.0.6'
# make: *** [Makefile.common:67: this-build] Error 2



<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
│ λ build coq-coqeal 1.0.6
└─ 

[ejgallego]

@thery can you post the contents (including hidden files) of $coqlib/user-contrib somewhere?

[thery]

@ejgallego Is a ls enough? There is one here

[ejgallego]

Yes, thanks @thery ; for some reason the ssr multinomials package is not enabling the native compiler so files [as you can see] are missing. I am not sure what the problem is, as there were may recent changes on the infrastructure to better support native.

Does an opam update + reinstall of multinomials fix it by any chance?

[ejgallego]

A possibility is that the coq-multinomials package was outdated on your system, that some dependency of such package is missing and thus not triggering the rebuild when coq-native is installed, or just some bug in the packaging.

[erikmd]

Hi @thery, I've just seen this issue and I think this is related to the fact multinomials is not yet released since it has been updated with coq-native support (math-comp/multinomials#45)
To sum up: coq-mathcomp-multinomials.1.5.4 is not coq-native compliant, but coq-mathcomp-multinomials.dev is fine.
So to use it before it is released, you may want to use in a local opam switch:

opam pin add -n -y -k git coq-mathcomp-multinomials.1.5.4 "https://github.com/math-comp/multinomials.git#master"
# the 1.5.4 above is a dummy version string: this trick allows to use dev as if it were 1.5.4 (for reverse deps)
opam install -j 2 coq-native coq-mathcomp-multinomials

[ejgallego]

Thanks @erikmd for the clarification; does this mean the non-compatible versions should conflict with coq-native?

That seems a bit heavy handed to be honest, but I dunno how to prevent that kind of situation.

[erikmd]

Hi @ejgallego, thanks for your comment!

I see what you mean: sometimes having a "conflict" can be useful to detect at opam-pre-install-time that a package will be incompatible.

However I don't think this would be needed (nor possible); to sum up:

• coq-native can be made compatible with every library built with coq_makefile:

  • either with no modification of the .opam file nor the project code if coq ≥ 8.13;
  • or (for coq < 8.13) with a small modification of the opam-coq-archive's .opam file (just by adding the COQEXTRAFLAGS line involved in PR https://github.com/coq/opam-coq-archive/pull/1835/files)
  • and likewise for the dependencies of this library, as the requirement of generating the .coq-native/* files is transitive.

• coq-native can also be made compatible with libraries built with Dune:

  1. if dune ≥ 2.8
  2. and coq ≥ 8.12.1
  3. and a manual modification of the dune configuration is performed, adding (mode native) if it is supported (hence the need for some configure file), like PR https://github.com/math-comp/multinomials/pull/45/files

So I believe that the handling of potential CI failures related to the coq-native package is not that heavy:
if we spot some related CI failures or requests from devs to native-compile a specific library,
it suffices to check the constraints above for the dependencies of this library.

---

But maybe it would be very nice if the constraint (iii) above was lifted… I mean, ensuring that with a new version of dune:

• if "coqc -config" prints "COQ_NATIVE_COMPILER_DEFAULT=yes",
  (which will only be true when coq has been compiled with the coq-native package flag asking for native precompilation),
• then automatically, (mode native) would be assumed.

But I'm not really dune-savvy, so I don't know if this is easy to do currently? (you told me lately that Dune's architecture was about to evolve)

− Anyway, beyond the suggestion above to make (mode native) implied like coq_makfile: the (mode native) manual setting would stay useful in case coq has just been compiled with flag -native-compiler ondemand and we want to force native precompilation manually.

[ejgallego]

Dune's automatic detection will have to wait to 3.0 unfortunately, that likely means end of 2021 :/ But yes, this should hopefully happen automatically; note that dune internal changes for this to happen have been already been merged in Dune's main branch, I just need to finish the PR adding the ${coq:foo} variables.

I am not sure what (mode ...) should do when not present in a (coq.theory ...) field; likely doing native compilation by default then? This has a minor drawback tho, which is that .v compilation rules are delayed until coqc is available [thus less "paralellism"], but this is only a concern on composed developers builds where coqc is built too, and will likely have a very minor impact.

Indeed, it is great we fix the packages, but what I mean is that for packages that have been not fixed, shouldn't we add a conflict?

But I see your point, fixing the packages is the same amount of work than adding the conflict.

[proux01]

I am not sure what (mode ...) should do when not present in a (coq.theory ...) field; likely doing native compilation by default then?

That's the whole point of coq-native, this should default to what coqc -config says.

Note that, according to multinomial's author, we should get a release in the coming months : coq/platform#25 (comment) which, thanks to Erik's patch, should finally fix all that very painful mess that came after multinomial switched to dune.

We should indeed also add conflict clauses in the opam pacakges, I should open a PR.

[erikmd]

Thanks Pierre.
But when you say:

We should indeed also add conflict clauses in the opam packages

What kind of conflit do you have in mind? as mentioned in my previous comment, I don't think these conflict clauses are useful in general for coq-native.

[proux01]

The fact that current multinomials releases built with dune are incompatible with coq-native?

[ejgallego]

The fact that current multinomials releases built with dune are incompatible with coq-native?

Technically they are not, their dependencies are.

[proux01]

Right. However, declaring all their dependencies as conflicting requires much more work, so maybe not worth the effort.

[erikmd]

The fact that current multinomials releases built with dune are incompatible with coq-native?

Technically they are not, their dependencies are.

I guess this is the other way around:

no release of multinomial currently generates .coq-native/* files (because of dune)
so at first sight "it compiles with coq-native" but the reverse dependencies of multinomials fail to build from sources (e.g., coq-native + multinomials.1.5.4 + coqeal fails).

As a result, I believe that @proux01 was really right:

• for all libraries using dune such as coq-mathcomp-multinomials,
  as the fix is more tricky than with coq_makefile,
  it can be worth it to add a conflict clause saying that
  {coq-mathcomp-multinomials:version <= 1.5.4} conflicts with {coq-native:installed}
  and when coq-mathcomp-multinomials.1.5.5 will be released, the conflict clause could be relaxed:
  {coq-mathcomp-multinomials:version >= 1.5.5} conflicts with {coq-native:installed & coq:version < "8.12.1"}
• but for coq_makefile, it is much easier: changing the opam suffices to fix any coq_makefile-based library, as said above