Chelsea Edmonds (Oct 02 2020 at 04:40): Chelsea Edmonds (Oct 02 2020 at 04:40):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?
Mark Wassell (Oct 12 2020 at 08:44):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.
Jonathan Julian Huerta y Munive (Dec 16 2021 at 15:58):Hello, I have asked a question in StackOverflow about linking the Zarith library with OCaml to do code-generation via Isabelle/HOL with an M1 Mac Computer. I am at a point where I just need Isabelle to use a specific (opam) switch that I manually installed and not the one generated with isabelle ocaml_setup. If anyone has any input on which Isabelle-shell-variables to modify so that this works, please feel free to answer, comment, or provide suggestions on this topic.
Last updated: Apr 23 2024 at 08:19 UTC