I saw this in a GitHub Actions job on current master
:
"coqc" -q "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -R theories MMaps theories/AVL.v
COQC theories/AVL.v
File "./theories/AVL.v", line 1233, characters 0-59:
Warning: Warning: Removed file ./theories/AVL.vo
Error: Anomaly "Uncaught exception End_of_file."
Never seen this warning before, is it something new? Did a quick search in issues, but didn't find anything.
ah, what may be happening is that two make jobs get the same file. But this is strange since I have a make target like this in Makefile.coq.local
:
GLOBFILES = $(VFILES:.v=.glob)
target: $(GLOBFILES) $(VFILES) # more stuff here
# action here
So shouldn't make
take care of non-duplicating jobs?
OK, now I suspect there is a bug with coq_makefile
, the duplication of jobs also happens with the standard make -jX html
:
"coqc" -q "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -R theories MMaps theories/Interface.v
COQC theories/Interface.v
"coqc" -q "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -R theories MMaps theories/Raw.v
"coqc" -q "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -R theories MMaps theories/Facts.v
"coqc" -q "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -R theories MMaps theories/Positive.v
COQC theories/Raw.v
COQC theories/Facts.v
COQC theories/Positive.v
Coq's manual documents that make foo.vo bar.vo
duplicates job, and I might have seen other cases of the bug being worse
But I don't get your second log: is it showing duplicate jobs?
but there is no call with make X.vo Y.vo
here. The multiple-job-for-same-file thing occurs with only make -jX html
after generating Makefile.coq
.
Yes, the second log shows two processes doing coqc theories/Interface.v
Sorry for being dense, but these are 2 processes, not one printed verbosely?
"coqc" -q "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -R theories MMaps theories/Interface.v
COQC theories/Interface.v
Karl Palmskog said:
but there is no call with
make X.vo Y.vo
here. The multiple-job-for-same-file thing occurs with onlymake -jX html
after generatingMakefile.coq
.Yes, the second log shows two processes doing
coqc theories/Interface.v
probably because of the glob rule
this looks like the stuff:
# FIXME ?merge with .vo / .vio ?
$(GLOBFILES): %.glob: %.v
$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
I'd say the FIXME is on the right track. Shouldn't this at least say that it produces a .vo
file?
Paolo Giarrusso said:
Sorry for being dense, but these are 2 processes, not one printed verbosely?
"coqc" -q "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" -R theories MMaps theories/Interface.v COQC theories/Interface.v
yes, I checked that these are two separate processes at OS level.
the problem is that the files: pattern: deps
rule syntax only works for single target rules
https://www.gnu.org/software/make/manual/make.html#Static-Pattern
OK, so no obvious solution then, I guess I'll have to work around it somehow
maybe https://github.com/coq/coq/pull/16757 will work
ah, I tried that change locally, that seems to work (after changing Makefile.coq
), great!
But maybe it could be hacked into Makefile.coq.local
locally to avoid waiting for 8.17 and beyond...
if you have a wrapper makefile you can also do something like
html:
$(MAKE) -f Makefile.coq
$(MAKE) -f Makefile.coq html
to make sure that html is only called after coqc has run
right, but that's a bit less flexible than fully depending on the globs... this is what I already did in some projects
Last updated: Jun 08 2023 at 04:01 UTC