Rocq Call 2025 04 08 - rocq-prover/rocq GitHub Wiki

• 2025-04-08, 4pm UTC+2 (Paris time zone offset)
• https://rendez-vous.renater.fr/rocq-call

Topics

• location of rocq-prover and coq opam files (https://rocq-prover.zulipchat.com/#narrow/channel/237656-Rocq-devs-.26-plugin-devs/topic/location.20of.20the.20rocq-prover.20opam.20file, Gaëtan, 15min)

Roles

• Chairman:
• Secretary:
• Attending:

Notes

• attending: Gaetan Gilbert, Pierre Roux, Enrico Tassi

• location of rocq-prover and coq opam files (https://rocq-prover.zulipchat.com/#narrow/channel/237656-Rocq-devs-.26-plugin-devs/topic/location.20of.20the.20rocq-prover.20opam.20file, Gaëtan, 15min)

  some files like rocq-prover.opam and coq.opam are causing issues in the repo because they depend on external packages like stdlib

  why the rocq-prover package fixes version of rocq-core, while it doesn't fixes version of stdlib, maybe it should fix both or neither

  conclusion: make a pull request removing the packages from Rocq repo