You are not logged in.
Pages: 1
Dear All,
I updated my laptop using pacman -Syu. One of the changes was that the package coq was
changed into the package rocq. Because of the name change of coq into rocq this update
was expected to occur at some point. However, the result of this seems to be that a part of
the standard library was lost. E.g., "Require Import ZArith" used to work but no longer does.
This may be related to the fact that nowadays some files that used to be in the standard
library are now in a separate repository. I.e., https://github.com/rocq-prover/rocq vs
https://github.com/rocq-prover/stdlib.
Old package coq:
[chrisd@deskie machine2]$ ls /usr/lib/coq/theories/
Arith derive Lists Numbers Relations ssr Wellfounded
Array extraction Logic omega rtauto ssrmatching ZArith
Bool Floats micromega PArith setoid_ring Strings
btauto FSets MSets Program Setoids Structures
Classes funind NArith QArith Sets Unicode
Compat Init nsatz Reals Sorting Vectors
New package rocq:
[chrisd@lappie ~]$ ls /usr/lib/coq/theories/
Array Classes derive Floats Lists Program Setoids ssrmatching
BinNums Compat extraction Init Numbers Relations ssr Strings
What is the recommended way in archlinux to be able to use ZArith and
other parts of the StdLib?
Kind Regards,
Chris Dams
Offline
In the meantime I made an issue out of this in the archlinux gitlab.
https://gitlab.archlinux.org/archlinux/ … NjE5M30%3D
So, hopefully, this will be solved soon.
Offline
Pages: 1