HoTT doesn't depend on Stdlib

[proux01]

HoTT doesn't depend on Stdlib

[jdchristensen]

@proux01 In #2312 we've fixed the build issues in the CI. So I think this can be closed. If I've misunderstood, feel free to reopen.

[proux01]

Well, the point is that, since HoTT doesn't depend on Stdlib, you'd better only require coq-core and not the metapackage coq (= coq-core + coq-stdlib), that will save you about 10 min of compilation time.

[proux01]

(but apparently, github doesn't enable me to reopen)

[jdchristensen]

@proux01 Reopened. This PR had no description, so I thought it was just about fixing a build error. Can you edit the first message to give a description?

@Alizter You said that your similar PR #2297 wasn't needed any more. But if we can speed up compilation with a change like this PR or your PR, that would be great. Can you comment on this PR and/or yours?

I don't know enough about dune to know which way makes the most sense.

[proux01]

Indeed, if the opam file is generated by dune you need to edit the source too (that's a pain)

[Alizter]

I am being careful. Morally we don't depend on coq-stdlib, but coqc -boot -version doesn't even work in 9.0 without the stdlib present. Having the stdlib dependency around is my way of being careful. If however this is no longer the case, I would welcome it.

Regarding the opam file vs dune-project file, my change in the other PR made the opam template the single source of package deps, mainly because dune was generating nonsense deps for Coq. that should aid the change here.

Coq was for a long time shipped as a whole package. This was changed recently, but via my testing around the time I wrote that PR, the separation was not as useful as I had hoped. We were still getting internal exceptions from Coq due to the absence of the stdlib. Dune makes various assumptions about how Coq works and how it finds libraries, so when these changed in Coq it broke the functionality of Dune. (Dune does things like passing -boot and this interacted badly with coqc --version, coqdep --version etc.)

I got a bit frustrated trying to track down all the issues and ultimately ran out of time. I regret that during the Coq -> Rocq transition there was little attention to how Dune was to transition. That was not within my scope of responsibilities to fix however.

Presumably, the only reason the CI here is green is because we don't cover the problematic 9.0 release of Rocq. IIUC we are covering 8.19, 9.1 and master.

[jdchristensen]

Presumably, the only reason the CI here is green is because we don't cover the problematic 9.0 release of Rocq. IIUC we are covering 8.19, 9.1 and master.

If 9.0 is the only issue, can we change the dependencies so that the stdlib is required with 9.0, but not with other versions?

BTW, it looks to me like "supported" uses 8.19.2, "latest" uses 8.20.1, and "dev" uses the latest master branch. And it looks like 9.1 was just released, so we might want to add at least one build for that. (And maybe it's time to drop 8.19.2?)

[Alizter]

@jdchristensen I think its sensible to support latest versions, if people want a version of the library that is compatible with an older Coq version, they can find it in the Git history and our opam releases. You will need to tweak the CI files and perhaps the flake.nix file. I might be able to have a look this weekend if you need any assistance.

[jdchristensen]

@Alizter If you can handle these, that would be great, as I don't know how it works. But I think we should have two separate PRs: one that tries dropping the standard library (except for 9.0 if necessary), and one that bumps our minimum supported version to 8.20 (or 8.20.1?) and also tests 9.1.

[proux01]

I am being careful. Morally we don't depend on coq-stdlib,

Well, it's not just "morally", Rocq's CI actually confirms HoTT compiles without Stdlib (since 9.0).

but coqc -boot -version doesn't even work in 9.0 without the stdlib present. Having the stdlib dependency around is my way of being careful. If however this is no longer the case, I would welcome it.

With which version? Coq was split for a long time in coq-core and coq-stdlib packages, with the former being essentially useless without the later. This all changed with 9.0 where coq-core now provides Corelib, making it actually usable without Stdlib. (hence the disjunctive constraint in the current PR)

Regarding the opam file vs dune-project file, my change in the other PR made the opam template the single source of package deps, mainly because dune was generating nonsense deps for Coq. that should aid the change here.

Great, then it should be easy to just edit the .opam.template file.

Coq was for a long time shipped as a whole package. This was changed recently, but via my testing around the time I wrote that PR, the separation was not as useful as I had hoped. We were still getting internal exceptions from Coq due to the absence of the stdlib. Dune makes various assumptions about how Coq works and how it finds libraries, so when these changed in Coq it broke the functionality of Dune. (Dune does things like passing -boot and this interacted badly with coqc --version, coqdep --version etc.)

C.f. above, looks like pre 9.0 behavior.

I got a bit frustrated trying to track down all the issues and ultimately ran out of time. I regret that during the Coq -> Rocq transition there was little attention to how Dune was to transition. That was not within my scope of responsibilities to fix however.

(well, that whole dune story is a disaster but that's another issue, anyway it keeps working fine with the coq shims for now)

Presumably, the only reason the CI here is green is because we don't cover the problematic 9.0 release of Rocq. IIUC we are covering 8.19, 9.1 and master.

Not sure why 9.0 would be more problematic than 9.1 (the current PR predates 9.1).

[jdchristensen]

Side note: does opam build the contrib files? I seem to recall that contrib/SetoidRewrite.v depends on the standard library.

[jdchristensen]

@proux01 I added a comment to #2297 showing that Coq-HoTT doesn't build with coq-core 9.0. You wrote:

Rocq's CI actually confirms HoTT compiles without Stdlib (since 9.0).

I'm not sure why it is ok in the Rocq CI but not when I try. Are you sure the Rocq CI doesn't have the Stdlib in place while doing this build?

[proux01]

My bad, you need dependencies on both rocq-core (for Corelib) and coq-core (for coq shim, because of dune) since coq-core is only depending on rocq-runtime but not rocq-core (so that the coq-core package keeps doing what it did with Coq <= 8.20).

[jdchristensen]

Thanks for helping out, @proux01. I've fixed this using the template method in #2297, so I'll close this version.