Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

coq-rewriter-perf-SuperFast.dev failing in coq bench #167

Open
SkySkimmer opened this issue Dec 20, 2024 · 2 comments
Open

coq-rewriter-perf-SuperFast.dev failing in coq bench #167

SkySkimmer opened this issue Dec 20, 2024 · 2 comments

Comments

@SkySkimmer
Copy link
Contributor

example log https://coq.gitlabpages.inria.fr/-/coq/-/jobs/5098564/artifacts/_bench/logs/coq-rewriter-perf-SuperFast.NEW.opam_install.1.stdout.log
contents https://gist.github.com/SkySkimmer/1781b418899354ded0a41ab668b167a4
error message

- ROCQ compile src/Rewriter/Util/plugins/Ltac2Extra.v
- While loading initial state:
- Warning: Native compiler is disabled, -native-compiler ondemand option
- ignored. [native-compiler-disabled,native-compiler,default]
- File "./src/Rewriter/Util/plugins/Ltac2Extra.v", line 3, characters 0-45:
- Error:
- System error: "src/Rewriter/Util/plugins/././ltac2_extra_plugin.cmxs: No such file or directory"
- 
- Command exited with non-zero status 1

coq-rewriter succeeded in the same bench
ci-rewriter in Coq CI works fine (example https://gitlab.inria.fr/coq/coq/-/jobs/5099579) (it just does make https://github.com/coq/coq/blob/c280b340b8d44371aad663fec29442413c172607/dev/ci/ci-rewriter.sh#L13)

I don't know the differences well, any idea what's going on?

@JasonGross
Copy link
Collaborator

Bizarre. The relevant target is defined

$$($(1)_PERF_LOGS) : %.log : %.v $(PERF_DIR)/$(1).vo
.PHONY: perf-$(1)
perf-$(1):: $($(1)_PERF_LOGS)
endef

I believe, so is just equivalent to attempting to make particular vo files. Is the dependency of .vo files on the .cmxs file not getting correctly registered? Has the mechanism of storing / using the dependencies changed since the last time the bench succeeded? (Presumably coq-rewriter would also fail with -j100, and it just so happens that the files are made in the right order?)

@SkySkimmer
Copy link
Contributor Author

SkySkimmer commented Dec 20, 2024

Running locally I see in .Makefile-old.d

src/Rewriter/Util/plugins/Ltac2Extra.vo src/Rewriter/Util/plugins/Ltac2Extra.glob src/Rewriter/Util/plugins/Ltac2Extra.v.beautified src/Rewriter/Util/plugins/Ltac2Extra.required_vo: src/Rewriter/Util/plugins/Ltac2Extra.v /home/gaetan/dev/coq/coq/_build/install/default/lib/rocq-runtime/plugins/cc_core/cc_core_plugin$(DYNLIB) /home/gaetan/dev/coq/coq/_build/install/default/lib/rocq-runtime/plugins/ltac2/ltac2_plugin$(DYNLIB) src/Rewriter/Util/plugins/ltac2_extra_plugin$(DYNLIB) /home/gaetan/dev/coq/coq/_build/install/default/lib/coq-core/META /home/gaetan/dev/coq/coq/_build/install/default/lib/rocq-runtime/META /home/gaetan/dev/coq/coq/_build/install/default/lib/rocq-runtime/coqworker src/Rewriter/Util/plugins/META.coq-rewriter

ie it contains

src/Rewriter/Util/plugins/Ltac2Extra.vo src/Rewriter/Util/plugins/Ltac2Extra.required_vo: src/Rewriter/Util/plugins/ltac2_extra_plugin$(DYNLIB) src/Rewriter/Util/plugins/META.coq-rewriter

which seems correct

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants