Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:23): Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:23):Hi Matthieu!
Matthieu Sozeau (Oct 03 2018 at 16:23):Hi Zoe!
Matthieu Sozeau (Oct 03 2018 at 16:24):So you were in branch 8.8 which compiled and did a git merge of your branch, right?
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:24):Yes, almost.
Matthieu Sozeau (Oct 03 2018 at 16:25):You first did a git checkout -b my8.8 or something similar
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:25):I was in Coq-8.8 which was compiling (note that parallel make was falling -- not sure if this is relevant tho)
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:25):yes exactly
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:26):and then I did git pull origin zoe_safe-for-space
Matthieu Sozeau (Oct 03 2018 at 16:26):Yep
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:27):and I fixed the conflicts etc.
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:27):that was my status after the pull
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:28):ζ certicoq [git:(merge-8.8):(✗)] > git status
On branch merge-8.8
You have unmerged paths.
(fix conflicts and run "git commit")
(use "git merge --abort" to abort the merge)
Changes to be committed:
modified: theories/L6_PCPS/Ensembles_util.v
new file: theories/L6_PCPS/Heap/bounds.v
new file: theories/L6_PCPS/Heap/closure_conversion.v
new file: theories/L6_PCPS/Heap/closure_conversion_util.v
new file: theories/L6_PCPS/Heap/compat.v
modified: theories/L6_PCPS/Heap/heap.v
modified: theories/L6_PCPS/Heap/heap_defs.v
new file: theories/L6_PCPS/Heap/invariants.v
new file: theories/L6_PCPS/Heap/toplevel.v
modified: theories/L6_PCPS/cps_util.v
modified: theories/L6_PCPS/ctx.v
modified: theories/L6_PCPS/functions.v
deleted: theories/L6_PCPS/heap.v
deleted: theories/L6_PCPS/heap_defs.v
modified: theories/L6_PCPS/identifiers.v
modified: theories/L6_PCPS/logical_relations.v
modified: theories/L6_PCPS/shrink_cps_correct.v
modified: theories/L6_PCPS/size_cps.v
modified: theories/_CoqProject
Unmerged paths:
(use "git add <file>..." to mark resolution)
both modified: theories/L6_PCPS/Heap/cc_log_rel.v
both modified: theories/L6_PCPS/Heap/closure_conversion_correct.v
both modified: theories/L6_PCPS/Heap/heap_equiv.v
both modified: theories/L6_PCPS/Heap/space_sem.v
both modified: theories/L6_PCPS/List_util.v
both modified: theories/L6_PCPS/set_util.v
Can you look into theories/_CoqProject for the L4_deBruijn lines?
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:30):sure!
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:30):diff --git a/theories/_CoqProject b/theories/_CoqProject
index a6e6f30..87f4a5c 100644
--- a/theories/_CoqProject
+++ b/theories/_CoqProject
@@ -156,8 +156,16 @@ L6_PCPS/instances.v
L6_PCPS/Heap/heap.v
L6_PCPS/Heap/heap_defs.v
L6_PCPS/Heap/heap_equiv.v
+L6_PCPS/Heap/GC.v
L6_PCPS/Heap/space_sem.v
-#L6_PCPS/Heap/cc_log_rel.v
+L6_PCPS/Heap/cc_log_rel.v
+L6_PCPS/Heap/compat.v
+L6_PCPS/Heap/closure_conversion.v
+L6_PCPS/Heap/closure_conversion_util.v
+L6_PCPS/Heap/bounds.v
+L6_PCPS/Heap/invariants.v
+L6_PCPS/Heap/closure_conversion_correct.v
+L6_PCPS/Heap/toplevel.v
So nothing related to L4
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:31):yup :(
Matthieu Sozeau (Oct 03 2018 at 16:32):You're doing a sequential make?
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:32):yes
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:32):parallel gives me an error much earlier
Matthieu Sozeau (Oct 03 2018 at 16:33):What does make VERBOSE=1 report?
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:39):Nthing very different:
Warning: Notation _ ,, _ was already used. [notation-overridden,parsing]
File "./L4_deBruijn/L3_to_L3_eta.v", line 24, characters 15-28:
Error: Unable to locate library L4.expression.
make[2]: *** [L4_deBruijn/L3_to_L3_eta.vo] Error 1
make[1]: *** [all] Error 2
make: *** [all] Error 2
What is the command line though ?
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:41):make VERBOSE=1
Matthieu Sozeau (Oct 03 2018 at 16:41):And you see just that output ?
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:41):doesn't change much in the output
Matthieu Sozeau (Oct 03 2018 at 16:42):You should see what options are passed to coqc which is what interests me :)
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:42):aah :)
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:43):ζ certicoq [git:(merge-8.8):(✗)] > make VERBOSE=1
/Library/Developer/CommandLineTools/usr/bin/make -C libraries
/Library/Developer/CommandLineTools/usr/bin/make --no-print-directory -f "Makefile" pre-all
if [ "8.8.1" != "8.8.1" ]; then\
echo "W: This Makefile was generated by Coq 8.8.1";\
echo "W: while the current Coq version is 8.8.1";\
fi
/Library/Developer/CommandLineTools/usr/bin/make --no-print-directory -f "Makefile" real-all
make[2]: Nothing to be done for `real-all'.
/Library/Developer/CommandLineTools/usr/bin/make --no-print-directory -f "Makefile" post-all
/Library/Developer/CommandLineTools/usr/bin/make -C theories
/Library/Developer/CommandLineTools/usr/bin/make --no-print-directory -f "Makefile" pre-all
if [ "8.8.1" != "8.8.1" ]; then\
echo "W: This Makefile was generated by Coq 8.8.1";\
echo "W: while the current Coq version is 8.8.1";\
fi
/Library/Developer/CommandLineTools/usr/bin/make --no-print-directory -f "Makefile" real-all
"coqc" -q -R Compiler CertiCoq.Compiler -R common CertiCoq.Common -R L1_QuotedCoq CertiCoq.L1 -R L1g CertiCoq.L1g -R L2_typeStripped CertiCoq.L2 -R L2d_flattenedApp CertiCoq.L2d -R L2k_noCnstrParams CertiCoq.L2k -R L2_5_box CertiCoq.L2_5 -R L3_flattenedApp CertiCoq.L3 -R L4_deBruijn CertiCoq.L4 -R L6_PCPS CertiCoq.L6 -R ../libraries CertiCoq.Libraries -R L7 CertiCoq.L7 -R Extraction CertiCoq.extraction -R Runtime CertiCoq.runtime -R ../benchmarks CertiCoq.Benchmarks -R compcert compcert L4_deBruijn/L3_to_L3_eta.v
File "./L4_deBruijn/L3_to_L3_eta.v", line 18, characters 0-29:
Warning: Notation _ ,, _ was already used. [notation-overridden,parsing]
File "./L4_deBruijn/L3_to_L3_eta.v", line 24, characters 15-28:
Error: Unable to locate library L4.expression.
make[2]: *** [L4_deBruijn/L3_to_L3_eta.vo] Error 1
make[1]: *** [all] Error 2
make: *** [all] Error 2
does this help?
Matthieu Sozeau (Oct 03 2018 at 16:45):It looks fine. What about make theories/L4_deBruin/expression.vo
Matthieu Sozeau (Oct 03 2018 at 16:45):Without the typo
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:47):hmm, just that in the command line?
ζ certicoq [git:(merge-8.8):(✗)] > make theories/L4_deBruijn/expression.vo
make: *** No rule to make target `theories/L4_deBruijn/expression.vo'. Stop.
Ok. cd theories; make L4_deBruijn/expression.vo
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:50):compiles just fine, and also, after that, make goes through!
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:51):it fails later now:
ζ certicoq [git:(merge-8.8):(✗)] > make
/Library/Developer/CommandLineTools/usr/bin/make -C libraries
make[2]: Nothing to be done for `real-all'.
/Library/Developer/CommandLineTools/usr/bin/make -C theories
COQC L4_deBruijn/L4_to_L4_1_to_L4_2.v
File "./L4_deBruijn/L4_to_L4_1_to_L4_2.v", line 3, characters 15-23:
Error: Unable to locate library polyEval.
make[2]: *** [L4_deBruijn/L4_to_L4_1_to_L4_2.vo] Error 1
make[1]: *** [all] Error 2
make: *** [all] Error 2
Try make clean; make
Matthieu Sozeau (Oct 03 2018 at 16:53):It seems it's your dependencies that are wrong
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:58):yikes, it went back to the first error :(
File "./L4_deBruijn/L3_to_L3_eta.v", line 24, characters 15-28:
Error: Unable to locate library L4.expression.
make[2]: *** [L4_deBruijn/L3_to_L3_eta.vo] Error 1
make[1]: *** [all] Error 2
make: *** [all] Error 2
can I regenerate the dependencies somehow?
Matthieu Sozeau (Oct 03 2018 at 17:01):After you do make clean, the first line you should see when you do make VERBOSE=1 again should be: "coqdep" -dyndep var -f _CoqProject > ".coqdeps.d" || ( RV=$?; rm -f ".coqdeps.d"; exit $RV )
Matthieu Sozeau (Oct 03 2018 at 17:01):Do you see that?
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:03):Yes
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:03):ζ certicoq [git:(merge-8.8):(✗)] > make VERBOSE=1
/Library/Developer/CommandLineTools/usr/bin/make -C libraries
"coqdep" -dyndep var -f _CoqProject > ".coqdeps.d" || ( RV=$?; rm -f ".coqdeps.d"; exit $RV )
Somehow these must be wrong. Let me check for L3_to_L3_eta.v. Try: grep "^L4_deBruijn/L3_to_L3_eta.vo" .coqdeps.d
Matthieu Sozeau (Oct 03 2018 at 17:07):I'm getting: L4_deBruijn/L3_to_L3_eta.vo L4_deBruijn/L3_to_L3_eta.glob L4_deBruijn/L3_to_L3_eta.v.beautified: L4_deBruijn/L3_to_L3_eta.v common/Common.vo L3_flattenedApp/compile.vo L4_deBruijn/expression.vo
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:09):hmmm, I don't seem to have this file
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:09):which seems very sketchy
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:09):running make should create this file, no?
Matthieu Sozeau (Oct 03 2018 at 17:12):Yes.
Matthieu Sozeau (Oct 03 2018 at 17:12):What if you just do "coqdep" -dyndep var -f _CoqProject
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:12):btw, before trying to merge I cloned a fresh version of the repo and I'm working there
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:12):not sure if that's relevant
Matthieu Sozeau (Oct 03 2018 at 17:13):That shouldn't change a thing. But you never know :)
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:14):It succeeds in theories/
Matthieu Sozeau (Oct 03 2018 at 17:15):Yes, I mean in theories
Matthieu Sozeau (Oct 03 2018 at 17:15):What about the grep command?
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:18):ζ theories [git:(merge-8.8):(✗)] > "coqdep" -dyndep var -f _CoqProject | grep "^L4_deBruijn/L3_to_L3_eta.vo"
*** Warning: in file common/TermAbs_parametricity.v, declared ML module paramcoq has not been found!
*** Warning: in file common/TermAbs_parametricity.v, declared ML module paramcoq has not been found!
L4_deBruijn/L3_to_L3_eta.vo L4_deBruijn/L3_to_L3_eta.glob L4_deBruijn/L3_to_L3_eta.v.beautified: L4_deBruijn/L3_to_L3_eta.v common/Common.vo L3_flattenedApp/compile.vo L4_deBruijn/expression.vo
I guess the warnings come from stderr.
Matthieu Sozeau (Oct 03 2018 at 17:20):Yes that's fine.
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:20):So I guess, the problem is that make does not create the .coqdeps.d file
Matthieu Sozeau (Oct 03 2018 at 17:20):What if you make it yourself using "coqdep" -dyndep var -f _CoqProject > .coqdeps.d
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:20):yes just did that
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:21):goes through, let's see how far
Matthieu Sozeau (Oct 03 2018 at 17:21):Does coqdep (without the grep) return a non-zero exit code?
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:23):it gave me several warnings
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:25):But it doesn't seem to return a non-zero exit code
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:25):I get
ζ theories [git:(merge-8.8):(✗)] > echo $?
0
after I run "coqdep" -dyndep var -f _CoqProject
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:27):But in any case, that's already extremely helpful :)
Matthieu Sozeau (Oct 03 2018 at 17:27):Ok. It doesn't seem to write them to .coqdeps.d though, so the mistery is still complete :)
Matthieu Sozeau (Oct 03 2018 at 17:27):But at least you can compile
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:27):yes :)
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:27):I can investigate this more, at least I'm not stuck anymore
Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:28):Thank you so much!!
Matthieu Sozeau (Oct 03 2018 at 17:28):No problem!
Last updated: Feb 06 2023 at 05:03 UTC