[CakeML] Build problems
S.A.Owens at kent.ac.uk
Mon Apr 3 12:37:42 UTC 2017
The key thing is that there are s-exp encoders and decoders, so you don’t have to write code to build the s-expressions yourself. You will want to translate the encoder from HOL to CakeML and then try to port that to PolyML. This is a process that we would like to make more automatic than it is now.
> On 2017/04/03, at 13:32, Magnus Myreen <magnus.myreen at gmail.com> wrote:
> Hi Lars,
> Ramana knows about the s-expression parsing. I'll let him answer. I
> only know that part of that development is here:
> I believe the bootstrapped compiler is not currently setup to read in
> input in s-expression format. However, I suspect it should be a fairly
> easy interface to add, e.g. there could probably be a command-line
> argument that swaps the usual parser to the s-expression parser in the
> bootstrapped version.
> On 3 April 2017 at 14:28, Lars Hupel <hupel at in.tum.de> wrote:
>> Dear Magnus,
>>> Would the bootstrapped compiler work for you? The bootstrapped
>>> compiler runs from the Unix command line just like any compiler (e.g.
>>> gcc). You might want to use it through the s-expression parser rather
>>> than the usual parser which parses SML syntax, because it easier to
>>> pretty print to s-expressions in a way that will be parsed to exactly
>>> the same AST.
>> sounds useful. Is there any documentation or an example of this input
>> format? How can I build the bootstrapped compiler?
More information about the Users