[CakeML-dev] location in HOL parser

[Ramana Kumar]

Having read about it a little bit, I don't think we would need to go
to anything as heavyweight as git submodules or using the repo tool.
The only thing we would need to do is:
- Add a HOL repo SHA to the CakeML repo (e.g., in some file)
- Make the regression test build HOL at that SHA
This would replace the status quo of "CakeML should be built with
whatever is the tip of HOL4's master" with "CakeML should be built
with the version of HOL4 indicated <here>".
Advantage: decouple breaking HOL changes from CakeML fixes
Disadvantage: a little more bookkeeping work required for local clones
(must keep your HOL clone matching the desired CakeML clone) and
someone should update the SHA from time to time (maybe only when
necessary) - arguably these things are already happening in a less
explicit way though

On 7 February 2017 at 12:20,  <Michael.Norrish at data61.csiro.au> wrote:
> 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
>
>
>
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers