Re: [isabelle] Scala code generator: how to write code generated from Isabelle library dependencies to a shared package?
- To: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>
- Subject: Re: [isabelle] Scala code generator: how to write code generated from Isabelle library dependencies to a shared package?
- From: Christoph LANGE <math.semantic.web at gmail.com>
- Date: Thu, 08 Aug 2013 16:47:46 +0200
- Cc: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>
- In-reply-to: <51DA5FD5.firstname.lastname@example.org>
- Organization: University of Birmingham
- References: <51D9C9FE.email@example.com> <51DA5FD5.firstname.lastname@example.org>
- Sender: Christoph Lange <allegristas at gmail.com>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130807 Thunderbird/17.0.8
thanks for your help, and sorry for replying so late. I was at a
conference and on holiday and only resumed working with generated code
2013-07-08 08:44 Andreas Lochbihler:
> The code generator always outputs all code for what is needed to
> implement the specified constants. From a modularity point of view, this
> is a bit unsatisfactory. I usually use one of two workarounds:
> a) Do not use module_name when exporting code. Then, the code generator
> puts every theory into a separate module (you can configure this to some
> extent with code_modulename). Unless you have naming conflicts between
> your theories, this should give you the same object Set for A.thy and
> B.thy (if both use the same operations on sets). This works particularly
> well for Haskell because the code generator already puts every module
> into a separate file. So if you set the same output directory for A and
> B, you just get the module once. For SML and Scala, all modules are in a
> single file for A and once more in a single file for B. But you can just
> split the files at the module boundaries with a simple script.
This is what I will try for now.
I wrote the following script; feel free to reuse it.
(user: guest, password: guest)
For now please bear with the access control, but we are planning to move
I will also make the script available in a nicer way at
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701
→ Mathematics in Computer Science Special Issue on “Enabling Domain
Experts to use Formalised Reasoning”; submission until 31 October.
This archive was generated by a fusion of
Pipermail (Mailman edition) and