myreen

Linking to sig files is fine by me. I hope browsers can be made aware that they ought to treat these as normal text files.

It might be better to target stackLang after a few shallow-to-shallow transformations within phase 1. The advantage is that then one can influence the stack size immediately (e.g. use one...

This is similar to #580

@charguer Having your help in writing the semantics is most appreciated! Regarding style: I think it's most important that the Coq definitions are nice to work with in Coq and...

@cmr: The new [CakeML compiler explorer](https://github.com/Saser/cakeml) might aid a bit in producing symbols for profiling. The project is due to finish in mid-May. However, they are unlikely to get through...

This sounds like a good idea to me. In your text, you say that this is "to be done in closLang". I agree that it cannot be done later for...

Ah, that makes sense. You are right that certain datatype constructors that are strictly different at source and FlatLang might turn into the same representation in ClosLang and thus allow...

The commits in #889 make progress on this issue. However, the commits in #889 do not attempt to lift the constants.

One could address a slightly broader question: should the translator mangle names at all and if so how? The current way it changes constructor names is a bit arbitrary. Note...

Sounds good. A first step would be to get a HOL export from sail into `HOL/examples`.