Re: [Gcl-devel] GCL and LLVM

[u1204]

Camm,

>Greetings!  I had looked briefly at having gcl compile to the gcc
>intermediate form, and ship it as a gcc front end, but did not get very
>far.  As I understand that LLVM also interfaces with gcc here, this
>would likely be the path to an llvm connection.  But it seems this
>should not stand in the way of your project, as both LLVM and GCL (and
>hence acl2) have C as a common target.

Well, right. But you and I both know that the issue will be the
compiler switches and other "trivial issues", likely to burn up a
month or so of fribitzing around. Sigh.

The time has come to prove something so ... let the fribitzing begin.
>
>BTW, is there a stable axiom release past 20120501 that I should package
>for Debian?

Most of the work last year was enhancing the computer algebra test
suite portion of Axiom with Albert Rich's integrals. Other than that
I've been swallowing code into the books, another set of changes that
are not really user-visible. But a new release should happen.

I will roll out a new release and send you an email when it is ready.

Tim

>
>address@hidden writes:
>
>> Camm,
>>
>> I've begun working on proving an Axiom algorithm. I'm looking
>> at Coq to work the proof at the Spad level and ACL2 to work the
>> proof at the Lisp level.
>>
>> Hardin, et.al [Hard14] has published a paper on an LLVM-to-ACL2
>> translator. Since GCL generates C, this looks like a way to
>> bridge the proof from Lisp to the hardware.
>>
>> So, the question is, have you tried hosting GCL on LLVM?
>>
>> Tim
>>
>> [Hard14] Hardin, David S.; Davis, Jennifer, A.; Greve, David A.;
>>          McClurg, Jedidiah R.
>> ``Development of a Translator from LLVM to ACL2''
>> http://arxiv.org/pdf/1406.1566
>