c-parser: update release script and README

tools/c-parser/INSTALL

@@ -1,5 +1,3 @@
-#
-#
 # Copyright 2014, NICTA
 #
 # This software may be distributed and modified according to the terms of
@@ -7,27 +5,52 @@
 # See "LICENSE_BSD2.txt" for details.
 #
 # @TAG(NICTA_BSD)
-#
-#
-# Installation Instructions for the C-Parser
+
+# Installation instructions for the C parser
+
+NB: These instructions apply to the stand-alone release of the C parser.
+If this is in an L4.verified checkout, see the top-level README instead.
 
 This code requires Isabelle2018 and the MLton SML compiler.
 
+The C parser supports multiple target architectures:
+
+    - ARM
+    - ARM_HYP
+    - X64
+
+These platforms differ in integer sizes and various other details.
+Choose your desired architecture using the L4V_ARCH environment variable:
+
+    export L4V_ARCH=ARM
+
 To build the main heap CParser, use the following command in this directory (src/c-parser).
 
-    isabelle env make -f IsaMakefile CParser
+    isabelle env make CParser
 
 You can also build a regression test with the command
 
-    isabelle env make -f IsaMakefile CParserTest
+    isabelle env make cparser_test
 
-## Other Tools
+The regression test may require a lot of memory to run. If your computer has
+enough memory, configure your etc/settings file to use a 64-bit runtime:
+
+    ML_PLATFORM=$ISABELLE_PLATFORM64
+    ML_HOME=$(dirname "${ML_HOME}")/$ML_PLATFORM
+
+## Loading the parser
+
+The ROOTS file for the parser is in the src directory.
+Run Isabelle with this directory as an argument, e.g.:
+
+    isabelle jedit -d src -l CParser foo.thy
+
+If that worked, then the C parser has been loaded successfully.
+See the README and PDF documentation for further instructions.
+
+## Other tools
 
 There are two executables that can be built in the standalone-parser directory:
 
     make standalone-cparser
     make standalone-tokenizer
-
-## Using the C Parser
-
-Theories wishing to use the parser must have CTranslation as an ancestor.

tools/c-parser/Makefile

@@ -30,7 +30,7 @@ cparser_tools: stp_all
 # Setup heaps we use.
 HEAPS += Simpl-VCG CParser
 
-# l4v root dir. Will be "." if this is a separate C parser release.
+# l4v root dir. Will be ".." if this is a separate C parser release.
 L4V_ROOT_DIR = ../..
 
 # Path to Isabelle

tools/c-parser/README

@@ -19,6 +19,9 @@ To use:
 3. Load ('install') C files into your theories with the Isar command
    install_C_file.
 
+See docs/ctranslation.pdf for more information about the options
+and C language semantics that this tool provides.
+
 See many examples in the testfiles directory.  For example,
 breakcontinue.thy is a fairly involved demonstration of doing things
 the hard way.

tools/c-parser/mkrelease

@@ -20,7 +20,6 @@ case $(uname) in
 esac
 
 
-
 warn ()
 {
   echo "$1" >&2
@@ -42,6 +41,7 @@ fi
 # Get the directory that this script is running in.
 CPARSER_DIR=$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )
 TOPLEVEL_DIR=$( git -C ${CPARSER_DIR} rev-parse --show-toplevel)
+RELEASE_ARCHS='ARM ARM_HYP X64'
 pushd "${TOPLEVEL_DIR}"
 
 # Ensure that our working directory is clean.
@@ -90,12 +90,33 @@ git -C "${TOPLEVEL_DIR}" ls-files -z | tr '\0' '\n' |
    tar -v -T - -c -f - -l |
   (cd "$outputdir/src" ; tar xf -)
 
+echo "Getting theory dependencies"
+CPARSER_DEPS=$(tempfile)
+for ARCH in $RELEASE_ARCHS; do
+    L4V_ARCH=$ARCH misc/scripts/thydeps -I ./isabelle -d . -b . -r CParser
+done |
+    sort -u >"$CPARSER_DEPS"
+
+if grep -q -vE '^(lib/|tools/c-parser/)' "$CPARSER_DEPS"; then
+    echo >&2 'unexpected dependencies outside lib/ and tools/c-parser/:'
+    grep >&2 -vE '^(lib/|tools/c-parser/)' "$CPARSER_DEPS"
+    exit 1
+fi
+
 echo "Copying misc files"
-find tools/c-parser/CTranslation.thy tools/c-parser/testfiles -name '*.thy' |
-    xargs '-d\n' misc/scripts/thydeps -T text -o - |
-    grep '^lib/' |
+grep '^lib/' "$CPARSER_DEPS" |
     xargs '-d\n' cp -v --parents -t "$outputdir/src"
 
+# other misc files
+cp -v --parents -t "$outputdir/src" \
+   lib/Word_Lib/ROOT
+
+echo "Creating ROOTS file"
+cat >"$outputdir/src/ROOTS" <<EOF
+lib/Word_Lib
+c-parser
+EOF
+
 echo "Rearranging directories"
 /bin/mv -v "$outputdir/src/tools/c-parser/README" "$outputdir"
 /bin/mv -v "$outputdir/src/tools/c-parser" "$outputdir/src/"
@@ -105,13 +126,13 @@ echo "Removing files"
 /bin/rm -v "$outputdir/src/c-parser/testfiles/many_local_vars".{c,thy}
 
 echo "Executing gen_isabelle_root to generate testfiles/\$L4V_ARCH/ROOT."
-for L4V_ARCH in ARM ARM_HYP RISCV64 X64; do
+for L4V_ARCH in $RELEASE_ARCHS; do
     python misc/scripts/gen_isabelle_root.py -i "$outputdir/src/c-parser/testfiles" -i "$outputdir/src/c-parser/testfiles/${L4V_ARCH}" -o "$outputdir/src/c-parser/testfiles/$L4V_ARCH/ROOT" -s CParserTest -b CParser ||
         die "gen_isabelle_root failed."
 done
 
 echo "Executing gen_isabelle_root to generate testfiles/all_tests_\$L4V_ARCH.thy."
-for L4V_ARCH in ARM ARM_HYP RISCV64 X64; do
+for L4V_ARCH in $RELEASE_ARCHS; do
     python misc/scripts/gen_isabelle_root.py -T -o "$outputdir/src/c-parser/all_tests_${L4V_ARCH}.thy" -b CParser -i "$outputdir/src/c-parser/testfiles" -i "$outputdir/src/c-parser/testfiles/${L4V_ARCH}" ||
         die "gen_isabelle_root failed."
 done
@@ -130,18 +151,9 @@ if ! grep -q '^L4V_ROOT_DIR = ' "$outputdir/src/c-parser/Makefile"; then
     die "failed to process c-parser/Makefile"
 fi
 sed $SEDIOPT \
-    -e 's/^L4V_ROOT_DIR = .*$/L4V_ROOT_DIR = ./' \
+    -e 's/^L4V_ROOT_DIR = .*$/L4V_ROOT_DIR = ../' \
     "$outputdir/src/c-parser/Makefile"
 
-
-# We are moving the c-parser directory from the "tools/c-parser" directory to
-# the "c-parser" directory. Here we carry out a hack to fixup import paths of
-# the form "../../lib/A" by converting them into "../lib/A".
-echo "Fixing import paths."
-pushd "$outputdir/src/c-parser"
-find -name '*.thy' -execdir sed $SEDIOPT -E -e 's&\.\./lib/&lib/&g' '{}' ';'
-popd
-
 echo "Generating standalone-parser/table.ML"
 pushd "$TOPLEVEL_DIR/tools/c-parser" > /dev/null
 "$TOPLEVEL_DIR/isabelle/bin/isabelle" env make -f Makefile "$(pwd)/standalone-parser/table.ML" \