[CakeML-dev] Building the env-refactor branch

[Magnus Myreen]

On 15 February 2017 at 14:55, Yong Kiam <tanyongkiam at gmail.com> wrote:
> I am fixing the translation on CakeML 314a5e6 and HOL 572ce3d
>
> Those work fine with the (old?) parsing scripts.
>
> It would be helpful if you had a look at ml_progLib on env-refactor since I
> might have also inadvertently slowed it down by expanding things
> incorrectly.

I'm looking at it. I'll commit my edits to a branch off of
env-refactor (because my tinkering with ml_progLib is likely to break
the bootstrap).

Cheers,
Magnus

> On Wed, Feb 15, 2017 at 6:53 AM, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
> wrote:
>>
>> Yes unfortunately the parser is still broken because of location
>> information. I think Michael and maybe Hugo are working on it (Michael
>> fixed cmlPtreeConversion today, but not the Props yet apparently).
>>
>> On 15 February 2017 at 22:43, Magnus Myreen <magnus.myreen at gmail.com>
>> wrote:
>> > I'm on that commit and I seem to get the following error while
>> > building dependencies of the translator. -- Magnus
>> >
>> > Holmake: Linking cmlPtreeConversionPropsScript.uo to produce
>> > theory-builder executable
>> > <<HOL message: Created theory "cmlPtreeConversionProps">>
>> > error in quse
>> > /Users/mom22/cakeml-env/semantics/proofs/cmlPtreeConversionPropsScript.sml
>> > : HOL_ERR {message = "No consistent parse", origin_function =
>> > "typed_parse_in_context", origin_structure = "Parse"}
>> > error in load cmlPtreeConversionPropsScript : HOL_ERR {message = "No
>> > consistent parse", origin_function = "typed_parse_in_context",
>> > origin_structure = "Parse"}
>> > Holmake: Failed script build for cmlPtreeConversionPropsScript -
>> > exited with code 1
>> > Holmake: Finished recursive invocation in ../semantics/proofs
>> > Holmake: Finished recursive invocation in
>> > ../semantics/alt_semantics/proofs
>> >
>> > On 15 February 2017 at 12:15, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
>> > wrote:
>> >> I think it's c59c4caf4
>> >>
>> >> On 15 February 2017 at 18:04, Magnus Myreen <magnus.myreen at gmail.com>
>> >> wrote:
>> >>> Hi all,
>> >>>
>> >>> What is the correct HOL commit for building env-refactor?
>> >>>
>> >>> I'm asking because I hope to try to speed up ml_progLib, which is
>> >>> making the bootstrap translation ridiculously slow at the moment (on
>> >>> master). The improvement is best done on env-refactor because that
>> >>> branch will soon be merged into master (I hope).
>> >>>
>> >>> Cheers,
>> >>> Magnus
>> >>>
>> >>> _______________________________________________
>> >>> Developers mailing list
>> >>> Developers at cakeml.org
>> >>> https://lists.cakeml.org/listinfo/developers
>>
>> _______________________________________________
>> Developers mailing list
>> Developers at cakeml.org
>> https://lists.cakeml.org/listinfo/developers
>
>