[CakeML-dev] Building the env-refactor branch

[Magnus Myreen]

On 15 February 2017 at 14:57, Magnus Myreen <magnus.myreen at gmail.com> wrote:
> 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).

I accidentally pushed my change directly to env-refactor. The
translator directory builds with the improved ml_progLib. However, I
can't test other directories due to breakage caused by recent parser
changes.

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