[CakeML] Build problems

[Magnus Myreen]

Would it make sense to run the s-expression pretty printer inside the
logic of Isabelle/HOL. If that's the case, then maybe an OpenTheory
translation from HOL4 --> Isabelle/HOL might work. -- Magnus

On 3 April 2017 at 14:37, Scott Owens <S.A.Owens at kent.ac.uk> wrote:
> 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
>>>
>