search

mit-plv / bedrock2

A work-in-progress language and compiler for verified low-level programming
http://adam.chlipala.net/papers/LightbulbPLDI21/
MIT License
297 stars 45 forks source link

Preliminary work on expression compiler #344

Closed psvenk closed 1 year ago

psvenk commented 1 year ago

This is not ready to merge (and some conflicts still need to be resolved, anyway), but I figured that I would open a draft pull request for now after having sat on this code for a while.

samuelgruetter commented 1 year ago

I didn't manage to isolate the Qed typechecking failure bug, but at least, I found a workaround: https://github.com/mit-plv/bedrock2/commit/12a789ec7f543dec62e0bc1a6eece6569cf26c9a It just consists closing the current Section and starting a new Section whenever the bug occurs. But I don't consider this very nice code. So I would suggest the following alternative, which is good practice anyways: Split Optimize.v into two files, one for the definitions of the optimization functions (eg OptimizeDefs.v) and one for the proofs (eg OptimizeProofs.v). /cc @andres-erbsen

andres-erbsen commented 1 year ago

Ha this sure sounds like one of the tactics involved (probably dependent induction) does the wrong thing when referencing definitions that depend on section variables. Perhaps it needlessly generalizes the context but still uses the env reference that depends on pre-generalization context.

I agree with the proposed split, but it'd be nice to report the bug as well.

samuelgruetter commented 1 year ago

Ha this sure sounds like one of the tactics involved (probably dependent induction) does the wrong thing when referencing definitions that depend on section variables. Perhaps it needlessly generalizes the context but still uses the env reference that depends on pre-generalization context.

Yes, that's exactly what happens. Why it happens, that's a different question: I tried to reproduce it from scratch in an empty file, but the variations I tried all worked correctly, and my time budget is exceeded :sweat_smile: Next step would be to isolate it by simplifying the original file manually, or by throwing the bug minimizer at it, if you want to give it a try :wink:

andres-erbsen commented 1 year ago

Reported at https://github.com/coq/coq/issues/17555

samuelgruetter commented 1 year ago

Reported at coq/coq#17555

Cool :tada: While minimizing, did you find a better workaround than what I suggested above?

andres-erbsen commented 1 year ago

No, and i'm not really holding my breadth that there would be one.

psvenk commented 1 year ago

So I would suggest the following alternative, which is good practice anyways: Split Optimize.v into two files, one for the definitions of the optimization functions (eg OptimizeDefs.v) and one for the proofs (eg OptimizeProofs.v).

This did not work because the issue is dependence between the proofs and not dependence of the proofs on the definitions. So, I applied 12a789e with the Coq bug report linked in comments.