Re: [isabelle] Scala code generator: how to write code generated from Isabelle library dependencies to a shared package?



Hi Andreas,

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
today.


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.

https://codex.cs.bham.ac.uk/svn/langec/formare/code/auction/isabelle/Auction/code/split-scala-modules.pl
(user: guest, password: guest)

For now please bear with the access control, but we are planning to move
to Github.

I will also make the script available in a nicer way at
http://www.cs.bham.ac.uk/research/projects/formare/code/auction-theory/isabelle.

Cheers,

Christoph

-- 
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.
  http://cs.bham.ac.uk/research/projects/formare/pubs/mcs-doform/




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