CParser build fails

[sdconsta]

The file tools/c-parser/CTranslation.thy references three files that do not exist:

l4v/tools/c-parser/CTranslation.thy

Lines 66 to 68 in 3abbdd7

	ML_file "StrictC.grm.sig"
	ML_file "StrictC.grm.sml"
	ML_file "StrictC.lex.sml"

It looks like these files existed in 6.0.0, but were removed some time before 7.0.0.

From the l4v directory, I ran

$ ./isabelle/bin/isabelle build -d . AutoCorres
*** I/O error: StrictC.grm.sig (No such file or directory)
*** The error(s) above occurred in session "CParser" (line 17 of "ROOT")

[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.