[CakeML-dev] Building the env-refactor branch

[Yong Kiam]

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.


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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20170215/921759ef/attachment.html>