[CakeML-dev] Building the env-refactor branch

[Yong Kiam]

That's fine for me, I'm going to update CakeML+HOL only when I've finished
the translation directory (now getting stuck for non-pmatch reasons).

On Wed, Feb 15, 2017 at 9:49 AM, Magnus Myreen <magnus.myreen at gmail.com>
wrote:

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