require Arith and use RelationClasses (for stdlib#150 and stdlib#152)

[andres-erbsen]

Simple adaptation for rocq-prover/stdlib#152

I am not sure why I needed to Require Arith in the other file. Hopefully that change is acceptable regardless.

Thanks!

Edit: mystery solved: Require Arith is for rocq-prover/stdlib#150

[proux01]

@andrew-appel if CI here confirms this is indeed backward compatible, could we please consider merging it so that the upstream PR on Stdlib can get merged

[andrew-appel]

The dev version of Rocq fails with:
File "./progs64/io_os_connection.v", line 572, characters 10-36:
Error: Error: The reference FinFun.Injective_map_NoDup was not found in the current
environment.

Should I go ahead and merge anyway? What would be a compatible proof for Injective_map_NoDup?

[proux01]

Cc @andres-erbsen this doesn't seem perfectly backward compatible (would be better if we can avoid synchronous overlays)

[andrew-appel]

I can probably fix this next week. But what is a "synchronous overlay"?

[andres-erbsen]

FinFun.Injective_map_NoDup was moved to Lists.Finite.Injective_map_NoDup which is re-exported from FinFun in rocq-prover/stdlib#154 (changelog). I expect it would work to import FinFun and to refer to the lemma with the unqualified name.

However, I find it curious that rocq-prover/stdlib#154 passed the stdlib CI job for VST. If we had noticed the breakage, we would have added a compatibility wrapper at the old path. Does VST CI build more of VST than stdlib ci? Should we build more? (@proux01 is this the right file to look at?)

(If it's really a previous change to stdlib change that broke VST, i don't think a synchronous overlay would help here. This term refers to creating a pair of PRs that need to be merged "at the same time", e.g. to stdlib and VST. We have resorted to this in cases where compatibility with released versions is fine but it would be hard for e.g. VST to be compatible with stdlib master and stdlib master + the new stdlib PR at the same time.)

[andrew-appel]

It's likely that the rocq-prover's own CI does not run this "test2". Qroc's CI runs only a small subset of VST's CI.

Can someone tell me what opam commands I would have to issue in a fresh switch to build the dev version of Croq and then build VST in it? In fact, I can't even build a fresh switch without knowing what version of OCaml it's supposed to use, so let me rephrase the question: What opam commands will build a switch with the dev version of Qorc such that VST will build in it?

[proux01]

TL;DR: Looks like I first need to improve VST support in Stdlib CI, let me try to do it, hopefully by the end of the week.

Cc @andres-erbsen this doesn't seem perfectly backward compatible (would be better if we can avoid synchronous overlays)

I was under the assumption that the CI breakage here came from the current overlay not being backward compatible, making it a synchronous overlay: one that must be merged synchronously to the upstream PR since it is not backward compatible (that unfortunately happens a lot with Rocq plugins, but should be essentially avoidable for libraries)

Anyway, our main issue indeed seems to be the CI of Stdlib not testing enough. At the very least we should ensure it tests as much as the CI of Rocq.

It's likely that the rocq-prover's own CI does not run this "test2". Qroc's CI runs only a small subset of VST's CI.

Rocq's CI essentially runs make: https://github.com/rocq-prover/rocq/blob/master/dev/ci/scripts/ci-vst.sh

What opam commands will build a switch with the dev version of Qorc such that VST will build in it?

I'd say

opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
opam install coq.dev

should get you Rocq master + Stdlib master. You can even

opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
opam install coq-flocq.dev
opam install coq-coimpcert.dev

That being said, those dev packages are less maintained than the release repo so they can be a bit broken sometimes.

[andrew-appel]

@andres-erbsen XXX can you give me permission to push to this fork? Seems simpler than making a p.r. to your p.r. XXX Never mind about the permission, my local repo is in a state where I have to go forward with the p.r. to the p.r.

Indeed, the fix you propose does work. I have also updated some submodules. After I merge this one into master, I plan a new p.r. with:

• Fix all the Rocq 9 deprecations
• Stop using submodules for InteractionTrees and coq-ext-lib, just assume they're already installed by opam or whatever
• Put in a proper opam file for VST. I had assumed we didn't really need one because the "real" opam file is in the coq-released archive, but actually it would be good to have one just for the dependencies when building locally.

[andres-erbsen]

This permission box is checked (and was already when I went to look at it):

Thank you for working with us on this.

[andrew-appel]

Closing without merging, because it is subsumed into #825.

[proux01]

FYI I updated the Stdlib CI rocq-prover/stdlib#182 to align it with Rocq one, taht is basically doing make IGNORECOQVERSION=true IGNORECOMPCERTVERSION=true
Hopefully, this will limit reoccurences of issues like the current one in the future.