Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Install c-parser-to-simpl

view this post on Zulip Email Gateway (Aug 22 2022 at 09:30):

From: "lyj238@ios.ac.cn" <lyj238@ios.ac.cn>
Dear experts:

I want to install C-Parser, a translator of C into SIMPL:--- http://ssrg.nicta.com.au/software/TS/c-parser/

I want to install as suggested as follows:

This code requires Isabelle2013.

To build:

isabelle make

invoked in this directory should do everything required.

However, the following error occurs:

[lyj@localhost flashT]~/Isabelle2014/bin/isabelle make

Cannot execute Poly/ML in 32bit mode (missing shared libraries for

C/C++)

Using bulky 64bit version of Poly/ML instead

Unknown Isabelle tool: make
[lyj@localhost flashT]$

Could you please give me a hand? How to build this parser?

regards
lyj

lyj238@ios.ac.cn

view this post on Zulip Email Gateway (Aug 22 2022 at 09:30):

From: Lars Noschinski <noschinl@in.tum.de>
Starting with Isabelle 2014, there is no "isabelle make" anymore (and
the C-parser wouldn't work with 2014 anyway). You might want to use
AutoCorres instead, it includes a version of the C-parser compatible
with Isabelle 2014:

https://ssrg.nicta.com.au/projects/TS/autocorres/

-- Lars Noschinski

view this post on Zulip Email Gateway (Aug 22 2022 at 09:30):

From: Michael Norrish <Michael.Norrish@nicta.com.au>
If you can’t get the parser bundled with AutoCorres to do the trick, I can probably send you a 2014 tar ball (though this would almost certainly be exactly the same thing as that bundled with AutoCorres).

Michael

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

Last updated: Nov 21 2024 at 12:39 UTC