Bridge to gaia ordinals

[palmskog]

@Casteran wrote in #53:

Thanks for the opam release for Gaia! I've just intialized an experimental branch Bridge within a theories/Bridgesdirectory. My first objective is to tranfer for instance the associativity of multiplication (proven in Gaia) to hydra-battles.

Let's use this separate issue to discuss the organization and results for the bridge to gaia ordinals. Right now, Pierre is doing experimental work in a separate branch, but once he thinks it is ready to merge we should decide about file/package name and placement and CI.

@Zimmi48 gaia currently takes around 10 minutes to build in CI. If we set up a separate job to check the bridge, this means the whole hydra-battles CI jumps to around 13-14 minutes. Should we do this for all PRs? It may affect the velocity of hydra-battles development. If we do set up CI, I would favor doing a completely separate opam package that depends on both coq-gaia and coq-hydra-battles. Opinions?

[Zimmi48]

If you test this package only with released versions and with Nix , then caching will ensure that CI doesn't take that long.

[palmskog]

Sounds reasonable, but correct me if I mistunderstood @Zimmi48: for caching to work in our current Nix CI setup, both gaia and hydra-battles have to be in Nix-unstable packages, right?

Even so, there are some additional hurdles, namely, if we want to make the files depending on Gaia compiled by default by coq_makefile (i.e., running make). If we do this, casual users who want to play around with exercises and are not familiar with Dune will get stuck unless they have gaia installed. One alternative is to create a special target for building everything including the gaia bridge (e.g., make bridge), which we invoke only in Nix CI. But without ugly shell hackery, this means we have to duplicate _CoqProject content.

[Zimmi48]

in our current Nix CI setup, both gaia and hydra-battles have to be in Nix-unstable packages, right?

Right and if a new package is introduced that depends on both gaia and hydra-battles, there should be a Nix package for this one as well. In this case, it seems better to fall back to a standard standalone installation of the Coq Nix Toolbox.

Even so, there are some additional hurdles, namely, if we want to make the files depending on Gaia compiled by default by coq_makefile (i.e., running make). If we do this, casual users who want to play around with exercises and are not familiar with Dune will get stuck unless they have gaia installed. One alternative is to create a special target for building everything including the gaia bridge (e.g., make bridge), which we invoke only in Nix CI. But without ugly shell hackery, this means we have to duplicate _CoqProject content.

It's fine (and actually seems more reasonable) if the Nix package also uses the Dune setup. That being said, including the files depending on Gaia in _CoqProject still seems important for casual development. But I don't think we need to go through any hackery. For instance, if I only have Equations installed, which is the only dependency of the current ordinals part, I can run make -j4 theories/ordinals/Epsilon0/Epsilon0.vo and it works fine (only generates three coqdep warnings because it cannot find paramcoq, mathcomp-ssreflect and mathcomp-algebra on the loadpath). Therefore, for the casual user, we could define some make aliases for the various parts of the project.

[palmskog]

Fine by me to create Nix packages and use the full Nix toolbox (but the lightweight Nix CI setup is at the limit I can help out with).

I propose that we use the following directory organization and name mapping for consistency and uniqueness:

theories
├── additions
├── gaia
└── ordinals

-R theories/gaia gaia_hydras

If it's OK with @Casteran, I can do a pass over the Bridge branch and set up the above organization and opam package (coq-gaia-hydras). I also have some SSReflect proof improvements...

[Casteran]

It’s fine with me, thanks ! Pierre

Le 14 août 2021 à 14:12, Karl Palmskog @.***> a écrit :

Fine by me to create Nix packages and use the full Nix toolbox (but the lightweight Nix CI setup is at the limit I can help out with).

I propose that we use the following directory organization and name mapping for consistency and uniqueness:

theories ├── additions ├── gaia └── ordinals -R theories/gaia gaia_hydras If it's OK with @Casteran https://github.com/Casteran, I can do a pass over the Bridge branch and set up the above organization and opam package (coq-gaia-hydras). I also have some SSReflect proof improvements...

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/coq-community/hydra-battles/issues/55#issuecomment-898886577, or unsubscribe https://github.com/notifications/unsubscribe-auth/AJW6FCRLAHENNXTXXT7UI5DT4ZMT5ANCNFSM5CDJIC3Q. Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&utm_campaign=notification-email.

[palmskog]

OK, all packages are defined in the master branch here and are in extra-dev in the Coq opam archive. For testing of the gaia bridge in CI, I will now have to hand the baton to @Zimmi48 to do Nix wizardry.

[Casteran]

Thanks !!!

By the way, I added the following requirement to gaia/T1Bridge.v (draft ; not committed yet) From mathcomp Require Import zify.

Is there anything we should add in the dune or in any magic file ?

Le 15 août 2021 à 11:42, Karl Palmskog @.***> a écrit :

OK, all packages are defined in the master branch here and are in extra-dev in the Coq opam archive. For testing of the gaia bridge in CI, I will now have to hand the baton to @Zimmi48 https://github.com/Zimmi48 to do Nix wizardry.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/coq-community/hydra-battles/issues/55#issuecomment-899023833, or unsubscribe https://github.com/notifications/unsubscribe-auth/AJW6FCQKUSZRUXS25IOENLDT46DWTANCNFSM5CDJIC3Q. Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&utm_campaign=notification-email.

[palmskog]

@Casteran you will have to add the following line in coq-gaia-hydras.opam, just below the line saying "coq-gaia" {...}:

  "coq-mathcomp-zify"

[Zimmi48]

gaia, hydra-battles and addition-chains are now in nixpkgs. I have opened #58 to set up the Nix Toolbox and CI based on it.

[Zimmi48]

@palmskog You were worried about CI length: it turns out that the CI job that was already the lengthiest (building the documentation) is impacted by the addition of Gaia as a dependency, since it also needs to install all of hydra-battles dependencies. I'll open a separate issue about this.