[CakeML] Build problems

[Scott Owens]

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.

Scott

> 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:
> 
> https://github.com/CakeML/cakeml/blob/master/compiler/parsing/fromSexpScript.sml
> 
> 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.
> 
> Cheers,
> Magnus
> 
> 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?
>> 
>> Cheers
>> Lars
>>