The proofs's discuss from stepchowfun

proofs's Issues

coq 8.19.1 can't find `Coq.Arith.Gt` on Arch

Thought you might like to know. FWIW, just commenting-out the "Require" line causes Coq to fail on the proof t_local_closure_monotonic (attempt to save an incomplete proof).

└──5026:mgh@bree[0,0,4]: make
rm -f \
          .CoqMakefile.d \
          .lia.cache \
          CoqMakefile \
          CoqMakefile.conf \
          _CoqProjectFull
cp _CoqProject _CoqProjectFull
find proofs -type f -name '*.v' >> _CoqProjectFull
coq_makefile -f _CoqProjectFull -o CoqMakefile || (rm -f \
            .CoqMakefile.d \
            .lia.cache \
            CoqMakefile \
            CoqMakefile.conf \
            _CoqProjectFull; \
          exit 1)
make -f CoqMakefile || (rm -f \
            .CoqMakefile.d \
            .lia.cache \
            CoqMakefile \
            CoqMakefile.conf \
            _CoqProjectFull; \
          exit 1)
make[1]: Entering directory '/home/mgh/code/projects/stephan-boyer-proofs'
COQDEP VFILES
Warning: in file proofs/system_f/local_closure.v, library
         Coq.Arith.Gt is required and has not been found in the loadpath!
         [module-not-found,filesystem,default]
Warning: in file proofs/system_f/opening.v, library
         Coq.Arith.Le is required and has not been found in the loadpath!
         [module-not-found,filesystem,default]
COQC proofs/system_f/local_closure.v
File "./proofs/system_f/local_closure.v", line 9, characters 0-28:
Error: Cannot find a physical path bound to logical path Coq.Arith.Gt.

make[2]: *** [CoqMakefile:848: proofs/system_f/local_closure.vo] Error 1
make[2]: *** [proofs/system_f/local_closure.vo] Deleting file 'proofs/system_f/local_closure.glob'
make[1]: *** [CoqMakefile:417: all] Error 2
make[1]: Leaving directory '/home/mgh/code/projects/stephan-boyer-proofs'
make: *** [Makefile:8: verify] Error 1
┌┤ ...stephan-boyer-proofs (Thu Mar 28 07:30:03) 1 usr(s), up 17:30, load 0.67/32, avail. mem 40/62G
│ [M]
└──5027:mgh@bree[2,0,4]: uname -a
Linux bree 6.8.1-arch1-1 #1 SMP PREEMPT_DYNAMIC Sat, 16 Mar 2024 17:15:35 +0000 x86_64 GNU/Linux
┌┤ ...stephan-boyer-proofs (Thu Mar 28 07:30:04) 1 usr(s), up 17:30, load 0.67/32, avail. mem 40/62G
│ [M]
└──5028:mgh@bree[0,0,4]: coqc --version
The Coq Proof Assistant, version 8.19.1
compiled with OCaml 5.1.0
┌┤ ...stephan-boyer-proofs (Thu Mar 28 07:30:08) 1 usr(s), up 17:30, load 0.66/32, avail. mem 40/62G
│ [M]
└──5029:mgh@bree[0,0,4]: make --version
GNU Make 4.4.1

Recommend Projects