CParser build fails about l4v

[Xaphiosis]

Please look at l4v/tools/c-parser/Makefile : these files are meant to be autogenerated.
In l4v, can you run ./run_tests -v CParser and if that fails give us the error generated?

The build method for CParser is old and perhaps unexpected. If you look what run_tests does in detail, it's actually doing:
isabelle/bin/isabelle env make -f IsaMakefile CParser

This means the c-parser-deps target is missing from Makefile. We will look at fixing this. Meanwhile, you should be able to build CParser via run_tests, or as a workaround you can add the c-parser-deps target to all in tools/c-parser/Makefile.

Does this help?

[sdconsta]

UPDATE: I figured out that these files needed to be generated by make. So I ran

$ make c-parser-deps

in the tools/c-parser directory, which built these dependencies. It looks like this is also referenced in the Isabelle makefile here:

l4v/tools/c-parser/IsaMakefile

Lines 57 to 58 in 3abbdd7

	# Generate lexer and parser files for CParser
	CParser: c-parser-deps

But for some reason this is not being triggered when I build AutoCorres from the l4v directory.

[Xaphiosis]

When I do ./run_tests AutoCorres these files are rebuilt. What do you do when you "build AutoCorres"?

[sdconsta]

See my first post. (I updated it with the command I used)

[Xaphiosis]

OK, I can tell you that it is not expected that if you try build things with just Isabelle that they will work. There are other files coming in from other parts of the build system that the Isabelle build system can't handle on its own. For example, if you want to build CRefine, you need the C code the C parser will be parsing, which is generated by the seL4 build system, which you can't call out to from the Isabelle build system.

We expect Makefiles to be the main source of instructing the system on how to build things, and the run_tests system to put them in order and parallelise them. The Isabelle build system can only take you further once all dependencies you need exist.

That said, our Makefiles should work and what you noticed will need a fix to build c-parser-deps

[sdconsta]

I was just following the directions in the README and INSTALL files, which suggested that the Isabelle build system should suffice to build the C parser. So if the Isabelle build system alone is not sufficient to make all of the dependencies, then the documentation should reflect this.

[mbrcknl]

Yes, it looks like we need to update some documentation files to reflect the fact that we've removed generated files from the l4v repository:

• tools/autocorres/README.md suggests using isabelle build ....
• tools/c-parser/INSTALL also suggests using isabelle build ..., and is so old it even gets the directory layout wrong.

To me, the CParser IsaMakefile looks OK, but I'll test that today. The AutoCorres Makefile looks like it needs some dependencies on the CParser. I'll also have a look at that.

[mbrcknl]

@fidget324 Thanks for reporting!

[Xaphiosis]

@mbrcknl the c-parser IsaMakefile is fine, the Makefile is missing a dependency on c-parser-deps. Very happy for you to fix this, especially the stale docs.

@fidget324 I was not suggesting you are doing anything wrong, merely pointing out the reality of the present moment and how it comes about. If you find any more examples of stale/incorrect docs, please poke us again!

[sdconsta]

@Xaphiosis No problem, this is a great project 🥇 :).

[mbrcknl]

@Xaphiosis Ok, though I'm not sure I understand the intention of the split between the IsaMakefile and Makefile. The entire purpose of the latter seems to be to build c-parser-deps. I don't see anything else in there that would depend on c-parser-deps.

[Xaphiosis]

It's probably a historic leftover from back when IsaMakefiles were the main way to do things. From what I can see on my screen, if you remove the three files that were reported in this issue, then go into tools/c-parser and type make all it will say "nothing to be done for 'all'", but run_tests will correctly rebuild them by invoking the IsaMakefile. Adding c-parser-deps to the all target in the Makefile addresses that shortcoming.

[mbrcknl]

RIght, I guess I mentally filtered the all target. :-)

Anyhow, at some point, we (@JaphethLim or I) will try to do a few things to address this:

• Publish an Isabelle2017-compatible AutoCorres release.
• Update a few READMEs.
• Maybe consolidate the c-parser IsaMakefile into the Makefile.

[lsf37]

update: the release AutoCorres 1.4 (for Isabelle2017) is now available from https://ts.data61.csiro.au/projects/TS/autocorres/ and the README is updated. We still have a Makefile and a separate IsaMakefile in cparser.

[lsf37]

The IsaMakefile is now removed and part of the Makefile. This could all still be simplified a bit, but I think this particular issue at least can be closed.

[niuzhi]

hello @lsf37 @Xaphiosis @mbrcknl ,I have pulled the file（verification-manifest/12.0.0.xml） according to the repo, but the following error still exists. Can you help?
root@ubuntu:/home/ubuntu/verification# ls
graph-refine HOL isabelle l4v seL4

======================================================================
/home/ubuntu/verification/l4v/tools/c-parser/standalone-parser/../../../isabelle/bin/isabelle build -d ../.. -b -v CParser
Started at Fri Jul 23 07:19:16 GMT 2021 (polyml-5.8.1_x86_64_32-linux on ubuntu)
ISABELLE_BUILD_OPTIONS=""

ML_PLATFORM="x86_64_32-linux"
ML_HOME="/root/.isabelle/contrib/polyml-5.8.1-20200228/x86_64_32-linux"
ML_SYSTEM="polyml-5.8.1"
ML_OPTIONS="-H 1000 --maxheap 10000 --stackspace 64"

Session Pure/Pure
Session FOL/FOL
Session Tools/Tools
Session HOL/HOL (main)
Session HOL/HOL-Library (main timing)
Session HOL/HOL-Computational_Algebra (main timing)
Session HOL/HOL-Analysis (main timing)
Session HOL/HOL-Eisbach
Session HOL/HOL-Statespace
Session HOL/HOL-Word (main timing)
Session Lib/Word_Lib (lib)
Session Lib/Lib (lib)
Session C-Parser/Simpl-VCG
Session C-Parser/CParser
Building Word_Lib ...
Word_Lib: theory HOL-Eisbach.Eisbach
Word_Lib: theory HOL-Eisbach.Eisbach_Tools
Word_Lib: theory HOL-Library.Sublist
Word_Lib: theory HOL-Library.Prefix_Order
Word_Lib: theory Word_Lib.Hex_Words
Word_Lib: theory Word_Lib.Signed_Words
Word_Lib: theory Word_Lib.Norm_Words
Word_Lib: theory Word_Lib.WordBitwise_Signed
Word_Lib: theory Word_Lib.Word_Type_Syntax
Word_Lib: theory Word_Lib.Word_Syntax
Word_Lib: theory Word_Lib.Word_Lib
Word_Lib: theory Word_Lib.Enumeration
Word_Lib: theory Word_Lib.Word_Enum
Word_Lib: theory Word_Lib.Word_Setup_32
Word_Lib: theory Word_Lib.Word_Setup_64
Word_Lib: theory Word_Lib.HOL_Lemmas
Word_Lib: theory Word_Lib.More_Divides
Word_Lib: theory Word_Lib.Aligned
Word_Lib: theory Word_Lib.Word_Next
Word_Lib: theory Word_Lib.Word_EqI
Word_Lib: theory Word_Lib.Word_Lemmas
*** Timeout
Word_Lib FAILED
(see also /root/.isabelle/heaps/polyml-5.8.1_x86_64_32-linux/log/Word_Lib)

theory "Word_Lib.Enumeration"
1.911s elapsed time, 1.871s cpu time, 0.096s GC time
Loading theory "Word_Lib.Word_Enum" (required by "Word_Lib.Word_Lemmas_32" via "Word_Lib.Word_Lemmas_Prefix" via "Word_Lib.Word_Lemmas")
instantiation
word :: (len) enum
enum_word == enum_class.enum :: 'a word list
enum_all_word == enum_class.enum_all ::
('a word bool) bool
enum_ex_word == enum_class.enum_ex ::
('a word bool) bool
instantiation
word :: (len) enumeration_both
enum_alt_word == enum_alt :: nat 'a word option

theory "Word_Lib.Word_Enum"
1.227s elapsed time, 1.211s cpu time, 0.000s GC time
Loading theory "Word_Lib.Word_Setup_32" (required by "Word_Lib.Word_Lemmas_32")

theory "Word_Lib.Word_Setup_32"
0.131s elapsed time, 0.130s cpu time, 0.000s GC time
Loading theory "Word_Lib.Word_Setup_64" (required by "Word_Lib.Word_Lemmas_64")

theory "Word_Lib.Word_Setup_64"
0.134s elapsed time, 0.134s cpu time, 0.000s GC time
Loading theory "Word_Lib.HOL_Lemmas" (required by "Word_Lib.Word_Lemmas_32" via "Word_Lib.Word_Lemmas_Prefix" via "Word_Lib.Word_Lemmas" via "Word_Lib.Word_EqI" via "Word_Lib.Word_Next" via "Word_Lib.Aligned")

theory "Word_Lib.HOL_Lemmas"
3.275s elapsed time, 3.026s cpu time, 0.141s GC time
Loading theory "Word_Lib.More_Divides" (required by "Word_Lib.Word_Lemmas_32" via "Word_Lib.Word_Lemmas_Prefix" via "Word_Lib.Word_Lemmas" via "Word_Lib.Word_EqI" via "Word_Lib.Word_Next" via "Word_Lib.Aligned")

theory "Word_Lib.More_Divides"
0.502s elapsed time, 0.386s cpu time, 0.000s GC time
Loading theory "Word_Lib.Aligned" (required by "Word_Lib.Word_Lemmas_32" via "Word_Lib.Word_Lemmas_Prefix" via "Word_Lib.Word_Lemmas" via "Word_Lib.Word_EqI" via "Word_Lib.Word_Next")

theory "Word_Lib.Aligned"
10.004s elapsed time, 7.912s cpu time, 0.355s GC time
Loading theory "Word_Lib.Word_Next" (required by "Word_Lib.Word_Lemmas_32" via "Word_Lib.Word_Lemmas_Prefix" via "Word_Lib.Word_Lemmas" via "Word_Lib.Word_EqI")

theory "Word_Lib.Word_Next"
5.701s elapsed time, 5.123s cpu time, 0.121s GC time
Loading theory "Word_Lib.Word_EqI" (required by "Word_Lib.Word_Lemmas_32" via "Word_Lib.Word_Lemmas_Prefix" via "Word_Lib.Word_Lemmas")

theory "Word_Lib.Word_EqI"
7.590s elapsed time, 4.887s cpu time, 0.059s GC time
Loading theory "Word_Lib.Word_Lemmas" (required by "Word_Lib.Word_Lemmas_32" via "Word_Lib.Word_Lemmas_Prefix")
linarith_split_limit exceeded (current value is 9)
linarith_split_limit exceeded (current value is 9)
*** Interrupt
Simpl-VCG CANCELLED
CParser CANCELLED
Unfinished session(s): CParser, Simpl-VCG, Word_Lib

Finished at Fri Jul 23 07:22:14 GMT 2021
0:02:58 elapsed time, 0:02:12 cpu time, factor 0.74
Makefile:42: recipe for target 'CParser' failed
make: *** [CParser] Error 1