Skip to content

coqdep warnings default AsError#22253

Draft
SkySkimmer wants to merge 1 commit into
rocq-prover:masterfrom
SkySkimmer:coqdep-warn-error
Draft

coqdep warnings default AsError#22253
SkySkimmer wants to merge 1 commit into
rocq-prover:masterfrom
SkySkimmer:coqdep-warn-error

Conversation

@SkySkimmer

Copy link
Copy Markdown
Contributor

No description provided.

@SkySkimmer SkySkimmer added needs: changelog entry This should be documented in doc/changelog. request: full CI Use this label when you want your next push to trigger a full CI. labels Jul 10, 2026
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 10, 2026
@SkySkimmer

Copy link
Copy Markdown
Contributor Author

not sure what's going on in fiat_parsers, after JasonGross/coq-scripts#16 there are module not found errors (can also be seen in the log of a successful CI)
cc @JasonGross

for neural_net_interp it seems we're doing a partial build with less deps so the files with missing deps are not compiled
I guess this is a problem of rocq makefile invoking rocq dep once for all files it knows about instead of invoking it only for the files we want to compile

@SkySkimmer

Copy link
Copy Markdown
Contributor Author

vst problem seems to be that there are a bunch of unused files with incorrect (outdated?) Requires
eg https://github.com/PrincetonUniversity/VST/blob/cbee87efb4bee2b588f8321e16b4cb7664d5cf60/msl/extract.v#L1 should be Require VST.msl.tree_shares but since the file is unused compilation doesn't error.

Could be fixed by fixing those files (just the Requires), deleting those files, or restricting the coqdep call to actually used files at https://github.com/PrincetonUniversity/VST/blob/cbee87efb4bee2b588f8321e16b4cb7664d5cf60/Makefile#L914-L930

@andrew-appel opinions?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

needs: changelog entry This should be documented in doc/changelog.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant