Stream: CertiCoq

Topic: imported from gitter room coq/certicoq


view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:23):

Hi Matthieu!

view this post on Zulip Matthieu Sozeau (Oct 03 2018 at 16:23):

Hi Zoe!

view this post on Zulip 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?

view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:24):

Yes, almost.

view this post on Zulip Matthieu Sozeau (Oct 03 2018 at 16:25):

You first did a git checkout -b my8.8 or something similar

view this post on Zulip 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)

view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:25):

yes exactly

view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:26):

and then I did git pull origin zoe_safe-for-space

view this post on Zulip Matthieu Sozeau (Oct 03 2018 at 16:26):

Yep

view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:27):

and I fixed the conflicts etc.

view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:27):

that was my status after the pull

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Oct 03 2018 at 16:28):

Can you look into theories/_CoqProject for the L4_deBruijn lines?

view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:30):

sure!

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Oct 03 2018 at 16:31):

So nothing related to L4

view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:31):

yup :(

view this post on Zulip Matthieu Sozeau (Oct 03 2018 at 16:32):

You're doing a sequential make?

view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:32):

yes

view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:32):

parallel gives me an error much earlier

view this post on Zulip Matthieu Sozeau (Oct 03 2018 at 16:33):

What does make VERBOSE=1 report?

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Oct 03 2018 at 16:40):

What is the command line though ?

view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:41):

make VERBOSE=1

view this post on Zulip Matthieu Sozeau (Oct 03 2018 at 16:41):

And you see just that output ?

view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:41):

doesn't change much in the output

view this post on Zulip Matthieu Sozeau (Oct 03 2018 at 16:42):

You should see what options are passed to coqc which is what interests me :)

view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:42):

aah :)

view this post on Zulip 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

view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:43):

does this help?

view this post on Zulip Matthieu Sozeau (Oct 03 2018 at 16:45):

It looks fine. What about make theories/L4_deBruin/expression.vo

view this post on Zulip Matthieu Sozeau (Oct 03 2018 at 16:45):

Without the typo

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Oct 03 2018 at 16:48):

Ok. cd theories; make L4_deBruijn/expression.vo

view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:50):

compiles just fine, and also, after that, make goes through!

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Oct 03 2018 at 16:52):

Try make clean; make

view this post on Zulip Matthieu Sozeau (Oct 03 2018 at 16:53):

It seems it's your dependencies that are wrong

view this post on Zulip 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

view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 16:59):

can I regenerate the dependencies somehow?

view this post on Zulip 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 )

view this post on Zulip Matthieu Sozeau (Oct 03 2018 at 17:01):

Do you see that?

view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:03):

Yes

view this post on Zulip 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 )

view this post on Zulip Matthieu Sozeau (Oct 03 2018 at 17:06):

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

view this post on Zulip 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

view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:09):

hmmm, I don't seem to have this file

view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:09):

which seems very sketchy

view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:09):

running make should create this file, no?

view this post on Zulip Matthieu Sozeau (Oct 03 2018 at 17:12):

Yes.

view this post on Zulip Matthieu Sozeau (Oct 03 2018 at 17:12):

What if you just do "coqdep" -dyndep var -f _CoqProject

view this post on Zulip 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

view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:12):

not sure if that's relevant

view this post on Zulip Matthieu Sozeau (Oct 03 2018 at 17:13):

That shouldn't change a thing. But you never know :)

view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:14):

It succeeds in theories/

view this post on Zulip Matthieu Sozeau (Oct 03 2018 at 17:15):

Yes, I mean in theories

view this post on Zulip Matthieu Sozeau (Oct 03 2018 at 17:15):

What about the grep command?

view this post on Zulip 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

view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:18):

I guess the warnings come from stderr.

view this post on Zulip Matthieu Sozeau (Oct 03 2018 at 17:20):

Yes that's fine.

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Oct 03 2018 at 17:20):

What if you make it yourself using "coqdep" -dyndep var -f _CoqProject > .coqdeps.d

view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:20):

yes just did that

view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:21):

goes through, let's see how far

view this post on Zulip Matthieu Sozeau (Oct 03 2018 at 17:21):

Does coqdep (without the grep) return a non-zero exit code?

view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:23):

it gave me several warnings

view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:25):

But it doesn't seem to return a non-zero exit code

view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:25):

I get

ζ  theories [git:(merge-8.8):(✗)] > echo $?
0

view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:26):

after I run "coqdep" -dyndep var -f _CoqProject

view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:27):

But in any case, that's already extremely helpful :)

view this post on Zulip 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 :)

view this post on Zulip Matthieu Sozeau (Oct 03 2018 at 17:27):

But at least you can compile

view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:27):

yes :)

view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:27):

I can investigate this more, at least I'm not stuck anymore

view this post on Zulip Zoe Paraskevopoulou (Gitter import) (Oct 03 2018 at 17:28):

Thank you so much!!

view this post on Zulip Matthieu Sozeau (Oct 03 2018 at 17:28):

No problem!


Last updated: Feb 06 2023 at 05:03 UTC