[m-users.] CompCert C as a backend for Mercury ?

[Sean Charles (emacstheviking)]

Thanks!

> On 2 May 2022, at 15:35, Dirk Ziegemeyer <dirk at ziegemeyer.de> wrote:
> 
> Hi Sean,
> 
> just in case you need some more distractions with Coq, I can recommend the Software foundations series [1], Volume 1 and 2. There is also a volume 0 "Discrete Math in Coq (alpha)" [2] which might be a good starting point.
> 
> Dirk
> 
> [1] https://softwarefoundations.cis.upenn.edu/
> [2] https://cs.pomona.edu/classes/cs54/book/
> 
> 
>> Am 02.05.2022 um 15:14 schrieb Sean Charles (emacstheviking) <objitsu at gmail.com>:
>> 
>> IT was a long shit! 
>> 
>> :D
>> 
>> However, the fruits of my exploration this morning are such that I have now become interested in Coq, like I need more distractions.
>> 
>> THanks
>> 
>> 
>>> On 2 May 2022, at 13:25, Julien Fischer <jfischer at opturion.com> wrote:
>>> 
>>> 
>>> On Mon, 2 May 2022, Sean Charles (emacstheviking) wrote:
>>> 
>>>> Today I learned of:   https://compcert.org/
>>>> A formally verified C compiler. I wondered what exposure it has to the
>>>> erudite members of this thread, and more to the point, has anybody
>>>> tried to compile the output of the mercury compiler with it?
>>> 
>>> Not to my knowledge.  I was aware of its existence, but since its
>>> license does not allow commercial use and one of the things I do with
>>> Mercury is develop commercial software there didn't seem any compelling
>>> reason to look into it further.
>>> 
>>>> It would seem like a match made in heaven.
>>>> I will be downloading this compiler to see what I can do with it.
>>> 
>>> Just so you're aware: there's bit more to it than just doing
>>> 
>>>  $ ./configure --with-cc=ccomp
>>> 
>>> If you search the git repository for when we added support for clang**
>>> (circa 2011), that might give you some idea of what is required to use
>>> a new C compiler.
>>> 
>>> The obvious starting point is: can you successfully compile the Boehm
>>> GC with it?
>>> 
>>> Julien.
>> 
>> _______________________________________________
>> users mailing list
>> users at lists.mercurylang.org
>> https://lists.mercurylang.org/listinfo/users
>