Re: [isabelle] Export files generated by code_export to hard drive



> Am 30.04.2019 um 18:59 schrieb Makarius <makarius at sketis.net>:
> 
> Just out of curiosity: What happens with the content of the global
> ~/output_hs directory? Is it just for information, our do other tools
> take over the content?

It’s mainly for information, so that I can setup the corresponding Haskell code correctly. We’re trying to reason about LLVM programs in Isabelle/HOL. Right now im using llvm-hs[1] to generate an AST of LLVM code which I then use with Isabelle’s generated code for small test runs. All of this is in its early stages, so it’s useful to have a way to quickly export the generated code.

Gruß
Max

[1] https://hackage.haskell.org/package/llvm-hs



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.