[CakeML-dev] location in HOL parser

[Magnus Myreen]

> 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

I worry that there is a more serious disadvantage: Suppose person A
hacks on CakeML proofs and realises that a minor change in HOL is
needed/desired (e.g. L3 theories need updating), but notices that
recent changes in HOL by persons B and C break proofs in CakeML (e.g.
the stateful simpsets have changed). This blocks person A from pushing
the SHA forwards because that would require understanding how to fix
CakeML proofs w.r.t. the completely separate changes to HOL made by B
and C.

In this scenario, I guess the right thing for person A is to go
checkout an old version of HOL based on the working SHA for CakeML,
make the HOL changes on top of it, and update the CakeML SHA for HOL
to point at the commit that is now on top of an old version of HOL
(the old SHA from CakeML).

Cheers,
Magnus



On 7 February 2017 at 02:35, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
> 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
>
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers