[CakeML-dev] .lem files in the semantics

[Ramana Kumar]

Coordination is good, yes :)

Regarding the inferencer cheats - it is OK to introduce cheats on
master. My current understanding is: the requirement for master is
that it builds; cheat-free is the requirement for releases.

(It occurs to me that we should probably have a definitive easy way to
test if a full build contains cheats...
https://github.com/CakeML/cakeml/issues/164 would probably help - then
Holmake can tell you via its CHEATED message)

Let me know when the translator is the only thing left on env-refactor
- I'd be happy to look at it. (I might do so earlier, depending on how
other things are going.)

On 9 December 2016 at 01:23, Scott Owens <S.A.Owens at kent.ac.uk> wrote:
>
>> On 2016/12/07, at 22:44, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
>>
>> I would like to merge the FFI names pull request (which Johannes
>> mentioned - is that ok with you Scott?) but apart from that the
>> moratorium sounds fine, presuming it's not for very long. I read it
>> primarily as impetus to get env-refactor merged as soon as possible…
>
> Yeah. Also, if you do need to make a change, then if you coordinate with me, we can make sure to get the conflicts solved correctly.
>
>> What's left to be done before the merge?
>
> Inferencer proofs are currently cheated. The translator doesn’t work. modLang and conLang need tweaking. I’ll be working on the latter.
>
> Scott
>
>>
>> On 8 December 2016 at 03:21, Johannes Åman Pohjola <pohjola at chalmers.se> wrote:
>>> I will happily abide by this moratorium, with one exception: some minor
>>> changes to .lem files on the isse159 branch, that I hope to make a pull
>>> request for very soon. The change to the .lem files is basically just to
>>> replace nums with strings wherever they represent FFI indexes, which I hope
>>> is innocent enough to cause you little additional merging pain.
>>>
>>> /Johannes
>>>
>>>
>>>
>>> On 2016-12-07 16:57, Scott Owens wrote:
>>>>
>>>> Can we put a moratorium on modifying the .lem files of the master branch
>>>> until after the env-refactor branch is merged. Merging master into
>>>> env-refactor creates a bunch of conflicts when this has happened. It is
>>>> especially bad for the .lem files in the proofs subdirectory where the
>>>> env-refactor branch no longer uses .lem files. The changes are at a real
>>>> risk of being lost as the only practical way to resolve the conflicts is
>>>> with a git checkout —ours followed by an attempt to re-apply the changes.
>>>>
>>>> Scott
>>>> _______________________________________________
>>>> 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
>>
>> _______________________________________________
>> Developers mailing list
>> Developers at cakeml.org
>> https://lists.cakeml.org/listinfo/developers
>