search

coq-community / vscoq

A Visual Studio Code extension for Coq [maintainers=@rtetley,@huynhtrankhanh,@thery,@Blaisorblade]
MIT License
331 stars 68 forks source link

Manual testing on large developments #204

Open maximedenes opened 3 years ago

maximedenes commented 3 years ago

Play a bit with the extension on CompCert and Mathcomp, for example.

SkySkimmer commented 3 years ago

And document what is done for reproducibility

gares commented 3 years ago

I've pushed the famous SternBrocot_Zaux file, the nemesis of the STM.

fakusb commented 3 years ago

One example we should test is adding a new lemma or inserting tactics in the middle of a huge file.