I'm currently working on developing a lot of new definitions and basic lemmas for some combinatorial structures in Isabelle. Also am using locales. Down the track (probably in a year or so), its likely I'll want to use this formalisation to generate code for a few different algorithms, something I have not done in Isabelle before. Does anyone have any general tips for things I should be keeping in mind now as I'm setting up all the definitions, that would make code generation easier in the future?
I am not a locale or code generation expert but my suggestions are these: You shouldn't leave it until the end to introduce code generation; you should make sure it works up front. There have been some posts on the email list on code generation and locales. Finally, there might be some things that you can pick up by trawling the AFP.
Last updated: Sep 25 2021 at 09:17 UTC