Stream: Coq devs & plugin devs

Topic: Removed file warning

view this post on Zulip Karl Palmskog (Oct 30 2022 at 07:55):

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.

view this post on Zulip Karl Palmskog (Oct 30 2022 at 08:01):

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?

view this post on Zulip Karl Palmskog (Oct 30 2022 at 08:14):

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

view this post on Zulip Paolo Giarrusso (Oct 30 2022 at 09:13):

Coq's manual documents that make foo.vo bar.vo duplicates job, and I might have seen other cases of the bug being worse

view this post on Zulip Paolo Giarrusso (Oct 30 2022 at 09:15):

But I don't get your second log: is it showing duplicate jobs?

view this post on Zulip Karl Palmskog (Oct 30 2022 at 09:16):

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

view this post on Zulip Paolo Giarrusso (Oct 30 2022 at 11:39):

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

view this post on Zulip Gaëtan Gilbert (Oct 30 2022 at 11:42):

Karl Palmskog said:

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

probably because of the glob rule

view this post on Zulip Karl Palmskog (Oct 30 2022 at 11:45):

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?

view this post on Zulip Karl Palmskog (Oct 30 2022 at 11:50):

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.

view this post on Zulip Gaëtan Gilbert (Oct 30 2022 at 11:51):

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

view this post on Zulip Karl Palmskog (Oct 30 2022 at 12:03):

OK, so no obvious solution then, I guess I'll have to work around it somehow

view this post on Zulip Gaëtan Gilbert (Oct 30 2022 at 12:08):

maybe https://github.com/coq/coq/pull/16757 will work

view this post on Zulip Karl Palmskog (Oct 30 2022 at 12:12):

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...

view this post on Zulip Gaëtan Gilbert (Oct 30 2022 at 12:15):

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

view this post on Zulip Karl Palmskog (Oct 30 2022 at 12:17):

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: Dec 07 2023 at 17:01 UTC