[CakeML-dev] location in HOL parser

[Michael.Norrish at data61.csiro.au]

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.

Michael

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.)
    
    Cheers,
    Ramana
    
    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