coq: add support for -native-compiler yes

[Alizter]

Description of changes

This patch adds support for enabling -native-compiler yes for Coq. As a result I have duplicated all the Coq packages for when we have the native compiler enabled. This is somewhat analogous to enabling flambda for OCaml, although there we don't have such a package set.

I am still uncertain if we want the extra package sets and I think we could probably deduplicate some things, but I am not sure if that is something we would want to do.

cc @NixOS/coq and perhaps @CohenCyril and @proux01 if they are interested.

Things done

• Built on platform(s)
  • x86_64-linux
  • aarch64-linux
  • x86_64-darwin
  • aarch64-darwin
• For non-Linux: Is sandbox = true set in nix.conf? (See Nix manual)
• Tested, as applicable:
  • NixOS test(s) (look inside nixos/tests)
  • and/or package tests
  • or, for functions and "core" functionality, tests in lib/tests or pkgs/test
  • made sure NixOS tests are linked to the relevant packages
• Tested compilation of all packages that depend on this change using nix-shell -p nixpkgs-review --run "nixpkgs-review rev HEAD". Note: all changes have to be committed, also see nixpkgs-review usage
• Tested basic functionality of all binary files (usually in ./result/bin/)
• 23.05 Release Notes (or backporting 22.11 Release notes)
  • (Package updates) Added a release notes entry if the change is major or breaking
  • (Module updates) Added a release notes entry if the change is significant
  • (Module addition) Added a release notes entry if adding a new NixOS module
• Fits CONTRIBUTING.md.

[Zimmi48]

I'm surprised. Did you test that the packages actually build with native correctly? I would have expected OCaml to become a propagated dependency when Coq is in native-compiler=yes mode.

I have also some concerns regarding the naming choice for the derivation argument / attributes. People that are not well-informed might think that "native" is something much more basic (e.g., building Coq with ocamlopt rather than ocamlc) and might miss that it is "just" about enabling / building Coq libraries with the native compiler.

One way to test this PR would be to open a test PR on the coq-nix-toolbox where you add another genAttrs to this code to enable native:

https://github.com/coq-community/coq-nix-toolbox/blob/6cde214677d077ee89ca84e56d88226a05f3af57/.nix/fallback-config.nix#L21-L29

(and then you regenerate the nix actions with genNixActions, of course after updating the nixpkgs pin as documented in https://github.com/coq-community/coq-nix-toolbox#testing-coqpackages-updates-in-nixpkgs).

[proux01]

Great! Indeed, it would be nice to test this on coq-nix-toolbox.

[Alizter]

@Zimmi48 I did not test any native builds other than the stdlib yet. It's entirely possible I will have to make OCaml a propagated build.

I have also some concerns regarding the naming choice for the derivation argument / attributes. People that are not well-informed might think that "native" is something much more basic (e.g., building Coq with ocamlopt rather than ocamlc) and might miss that it is "just" about enabling / building Coq libraries with the native compiler.

Absolutely. I think renaming to nativeCompiler would perhaps be more sensible. I'm also not super convinced that having a coqNative mirror package is a good idea. Perhaps just allowing it to be configured would be enough. That way we wouldn't have to maintain packages and their native versions. It's not like OCaml flambda also has it's own package set, but you can generate it if you wish.

I'll look into making a coq-nix-toolbox PR.

• testing native config coq-community/coq-nix-toolbox#140

[Alizter]

Result of nixpkgs-review pr 224110 run on x86_64-linux 1

23 packages failed to build:

• coq_nativePackages.ITree
• coq_nativePackages.coq-ext-lib
• coq_nativePackages.coqeal
• coq_nativePackages.coquelicot
• coq_nativePackages.fourcolor
• coq_nativePackages.interval
• coq_nativePackages.mathcomp
• coq_nativePackages.mathcomp-algebra
• coq_nativePackages.mathcomp-analysis
• coq_nativePackages.mathcomp-bigenough
• coq_nativePackages.mathcomp-character
• coq_nativePackages.mathcomp-classical
• coq_nativePackages.mathcomp-field
• coq_nativePackages.mathcomp-fingroup
• coq_nativePackages.mathcomp-finmap
• coq_nativePackages.mathcomp-real-closed
• coq_nativePackages.mathcomp-solvable
• coq_nativePackages.ssreflect (coq_nativePackages.mathcomp-ssreflect)
• coq_nativePackages.mathcomp-zify
• coq_nativePackages.multinomials
• coq_nativePackages.paco
• coq_nativePackages.pocklington
• coq_nativePackages.stdpp

124 packages built:

• compcert (coqPackages.compcert)
• compcert.doc (coqPackages.compcert.doc)
• compcert.lib (coqPackages.compcert.lib)
• compcert.man (coqPackages.compcert.man)
• coq (coqPackages.coq ,coq_8_16)
• coqPackages.Cheerios
• coqPackages.CoLoR
• coqPackages.HoTT
• coqPackages.ITree
• coqPackages.InfSeqExt
• coqPackages.LibHyps
• coqPackages.QuickChick
• coqPackages.StructTact
• coqPackages.VST
• coqPackages.Verdi
• coqPackages.aac-tactics
• coqPackages.addition-chains
• coqPackages.autosubst
• coqPackages.bignums
• coqPackages.category-theory
• coqPackages.ceres
• coqPackages.coq-bits
• coqPackages.coq-elpi
• coqPackages.coq-ext-lib
• coqPackages.coq-lsp
• coqPackages.coq-record-update
• coqPackages.coqeal
• coqPackages.coqide
• coqPackages.coqprime
• coqPackages.coquelicot
• coqPackages.corn
• coqPackages.deriving
• coqPackages.dpdgraph
• coqPackages.equations
• coqPackages.extructures
• coqPackages.flocq
• coqPackages.fourcolor
• coqPackages.gaia
• coqPackages.gaia-hydras
• coqPackages.gappalib
• coqPackages.goedel
• coqPackages.graph-theory
• coqPackages.hierarchy-builder
• coqPackages.hydra-battles
• coqPackages.interval
• coqPackages.iris
• coqPackages.itauto
• coqPackages.math-classes
• coqPackages.mathcomp
• coqPackages.mathcomp-algebra
• coqPackages.mathcomp-algebra-tactics
• coqPackages.mathcomp-analysis
• coqPackages.mathcomp-apery
• coqPackages.mathcomp-bigenough
• coqPackages.mathcomp-character
• coqPackages.mathcomp-classical
• coqPackages.mathcomp-field
• coqPackages.mathcomp-fingroup
• coqPackages.mathcomp-finmap
• coqPackages.mathcomp-real-closed
• coqPackages.mathcomp-solvable
• coqPackages.ssreflect (coqPackages.mathcomp-ssreflect)
• coqPackages.mathcomp-tarjan
• coqPackages.mathcomp-word
• coqPackages.mathcomp-zify
• coqPackages.metacoq
• coqPackages.metacoq-erasure
• coqPackages.metacoq-pcuic
• coqPackages.metacoq-safechecker
• coqPackages.metacoq-template-coq
• coqPackages.metalib
• coqPackages.multinomials
• coqPackages.paco
• coqPackages.paramcoq
• coqPackages.parsec
• coqPackages.pocklington
• coqPackages.reglang
• coqPackages.relation-algebra
• coqPackages.semantics
• coqPackages.serapi
• coqPackages.simple-io
• coqPackages.stdpp
• coqPackages.tlc
• coqPackages.topology
• coqPackages.trakt
• coqPackages.zorns-lemma
• coq_8_10
• coq_8_11
• coq_8_12
• coq_8_13
• coq_8_14
• coq_8_15
• coq_8_17
• coq_8_5
• coq_8_6
• coq_8_7
• coq_8_8
• coq_8_9
• coq_native (coq_nativePackages.coq ,coq_native_8_17)
• coq_nativePackages.HoTT
• coq_nativePackages.bignums
• coq_nativePackages.coq-elpi
• coq_nativePackages.coqide
• coq_nativePackages.equations
• coq_nativePackages.flocq
• coq_nativePackages.hierarchy-builder
• coq_nativePackages.paramcoq
• coq_native_8_10
• coq_native_8_11
• coq_native_8_12
• coq_native_8_13
• coq_native_8_14
• coq_native_8_15
• coq_native_8_16
• coq_native_8_5
• coq_native_8_6
• coq_native_8_7
• coq_native_8_8
• coq_native_8_9
• easycrypt
• framac
• ligo
• satallax
• why3

[Zimmi48]

The PR will need some documentation, especially in the case where the native version is not available as attributes by default.

[proux01]

23 packages failed to build:
coq_nativePackages.coqeal
coq_nativePackages.interval
coq_nativePackages.mathcomp

Those are a bit worrying (mathcomp works in Coq CI for instance).

[Alizter]

@proux01 I didn't investigate what went wrong yet, but likely a missing dependency.

[vbgl]

The change to compcert is wrong.

Also you may want to fix #34657 before (possible fixes include: resolve the path to the compilers at (coq) build time; wrap the coq binaries).