[CakeML-dev] location in HOL parser

Michael.Norrish at data61.csiro.au Michael.Norrish at data61.csiro.au
Tue Feb 7 01:20:45 UTC 2017

A related issue is perhaps making use of HOL as a sub-repo (I’m not sure what the best git technology is for doing this).  This way we could pin our CakeML work to specific HOL4 SHAs and not have HOL work break CakeML. 

The l4.verified repos use some technology in this vein, and I think it’s strictly OK (it’s a tool called repo).  I don’t know if there are any other obvious contender solutions.


On 7/2/17, 12:12, "Ramana Kumar" <Ramana.Kumar at cl.cam.ac.uk> wrote:

    Hi Hugo,
    Thanks for fixing things. Yes, it's ok to have cheats in the sexp
    parser theory if you plan to fix them eventually (I can probably help
    with that).
    However, I realised that if we merge these changes to HOL, it will
    break CakeML master branch. Do you have something accommodating the
    changes to the parser on the CakeML side that's ready to merge too?
    Ideally we could get them both at roughly the same time.
    (I'm CC'ing Michael and Magnus. My understanding is that Magnus is
    stalled waiting on these changes (is that right?) so I don't want to
    delay things unnecessarily.)
    On 7 February 2017 at 04:54, Hugo Férée <H.Feree at kent.ac.uk> wrote:
    > Hi Ramana,
    > I have fixed my pull request so that travis successfully builds.
    > However, I had to comment out or cheat some correctness results in the
    > SExpression parser. I know that I can fix most of them, but not before a
    > few days, but there is a very long proof in the end for which I might
    > need help with it.
    > Is all this a problem for merging?
    > Best,
    > Hugo

More information about the Developers mailing list