search

kth-step / HolBA

Binary analysis in HOL
Other
33 stars 20 forks source link

Update to modern syntax #173

Closed didriklundberg closed 4 months ago

didriklundberg commented 4 months ago

@didriklundberg this looks good to me, but "local theorems" / trivialities are not converted. Will you convert prove("xyz", ... ) to Theorem xyz[local]: ... in these files in a future PR?

Good suggestion. I was planning to add more into this PR, depending on your feedback. I'll see how much work it is.

arolle commented 4 months ago

Looks good to me. Your automatic conversion covers the vast majority of occurrences. There are a few remaining ones, e.g. occurrences of prove in *Script.sml files that can be fixed by hand later.

This is ready to be merged, however as mentioned elsewhere there can be a couple of merge conflicts in the near future due to these changes. Any branches that remain to be merged into master should probably go before this PR, to simplify their merge.

arolle commented 4 months ago

In case you want to further improve your script (no need to!), here are some of the occurrences that seem to remain:

grep --recursive --include='*Script.sml' 'val.*=.*\(\<save_thm\>\|\<prove\>\)'
didriklundberg commented 4 months ago

I noticed some removed lemmas made a comeback...

My apologies, this must be from the rebase I did after merging #174