search

CakeML / cakeml

CakeML: A Verified Implementation of ML
https://cakeml.org
Other
929 stars 81 forks source link

Translator should use a custom compset #216

Open tanyongkiam opened 7 years ago

tanyongkiam commented 7 years ago

Currently, it makes use of [simp] and EVAL in ml_progLib to control the EVALs that in ml_translatorLib

xrchz commented 5 years ago

Could you be more specific about (a) what problems are caused by (b) what flaws in the codebase?

talsewell commented 5 years ago

I can be more specific. Many parts of the translator and characteristic Lib code make use of EVAL in particular to do ... all kinds of things.

There are a collection of fixmes around cfTacticsLib and cfTacticsBaseLib that acknowledge this, for instance.

It's convenient to use EVAL because it handles a lot of intermediate definitions without adding code for them. The problem is (as I discovered in the nsLookup work) the code isn't very stable or self-documenting. You can change definitions in various scripts that aren't obviously used anywhere, only to find out that EVAL is unfolding them in every cf proof everywhere.

It would be nice if these tools constructed a particular compset so that it was more clear how to keep their results stable under changes to other things.

talsewell commented 5 years ago

Also, while working on the nsLookup changes (issue #527 ) I struggled with this a lot, until I figured out how to add my new code as a conv to the global compset.

Along the way I wrote some code to try to figure out which EVAL-s required what, so I could use that to try to investigate. It's going to be pretty slow progress though.