Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] C-to-Isabelle multiple external files

view this post on Zulip Email Gateway (Mar 22 2021 at 10:23):

From: Adriana Stancu <>

I am not sure if this is the right mailing list for this question: I am
using C-to-Isabelle parser to include a small C program, the structure is
as follows:

external_file "bar.c"install_C_file "bar.c"
The functions from foo.c are not parsed, only the declaration of the
functions found in foo.h.
In parser output: Added external decl for timeout_set with 2 args. Where
timeout_set is a function declared in foo.h and implemented in foo.c
How can I include also the implementation of the functions found in foo.c
when parsing bar.c?

Best regards,
Adriana Stancu

view this post on Zulip Email Gateway (Mar 22 2021 at 10:41):

From: Thomas Sewell <>
It's possible that this has changed or been improved. However, when I
was working with it, the C-to-Isabelle parser needed to know the names
and types of all local and global variables in order to set up the state
type, so it needed to see all the C source.

The typical solution is simple and ugly: use the C preprocessor to
all the source files into a single target. The C-to-Isabelle parser runs
preprocessor, so you can do this by pointing it at a small C file that
contains #include directives for foo.c and bar.c.

Yes, it's not ideal. There are reasons it's hard to fix which I could
in more length, if anyone really cares.

Best wishes,

view this post on Zulip Email Gateway (Mar 22 2021 at 10:54):

From: Yakoub Nemouchi <>
Or use the better and more advanced/elegant/powerful C11-parsing framework
on a top on Isabelle which is:

Best wishes,


view this post on Zulip Email Gateway (Mar 23 2021 at 10:20):

From: Jaap Boender <>
I'd definitely be interested - it's certainly a limitation we'd like to get rid
of at some point, if at all possible.



Last updated: Sep 25 2021 at 09:17 UTC