diff --git a/tools/c-parser/INSTALL b/tools/c-parser/INSTALL index bddfdb97f..6bcf4eb15 100644 --- a/tools/c-parser/INSTALL +++ b/tools/c-parser/INSTALL @@ -9,7 +9,7 @@ # 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. +If this is in an L4.verified checkout, see the top-level README.md instead. This code requires Isabelle2018 and the MLton SML compiler. @@ -46,7 +46,7 @@ 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. +See the README.md file and PDF documentation for further instructions. ## Other tools diff --git a/tools/c-parser/README b/tools/c-parser/README.md similarity index 62% rename from tools/c-parser/README rename to tools/c-parser/README.md index 57d448ba9..e5a4a971a 100644 --- a/tools/c-parser/README +++ b/tools/c-parser/README.md @@ -1,31 +1,33 @@ -# -# Copyright 2014, NICTA -# -# This software may be distributed and modified according to the terms of -# the BSD 2-Clause license. Note that NO WARRANTY is provided. -# See "LICENSE_BSD2.txt" for details. -# -# @TAG(NICTA_BSD) -# + + +The StrictC translation tool +============================ + +To install, see the file INSTALL in the `src/c-parser` directory. To use: 1. Use the heap CParser that is created by installation 2. Import the theory CTranslation 3. Load ('install') C files into your theories with the Isar command - install_C_file. + `install_C_file`. -See docs/ctranslation.pdf for more information about the options +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 +See also the examples in the testfiles directory. For example, +`breakcontinue.thy` is a fairly involved demonstration of doing things the hard way. + ---------------------------------------------------------------------- The translation tool builds on various open source projects by others. @@ -34,7 +36,7 @@ The translation tool builds on various open source projects by others. Sources for this are found in the Simpl/ directory. The code is covered by an LGPL licence. - See http://afp.sourceforge.net/entries/Simpl.shtml + See https://isa-afp.org/entries/Simpl.shtml 2. Code from SML/NJ: - an implementation of binary sets (Binaryset.ML) diff --git a/tools/c-parser/mkrelease b/tools/c-parser/mkrelease index d8bd10c35..09e18b119 100755 --- a/tools/c-parser/mkrelease +++ b/tools/c-parser/mkrelease @@ -118,7 +118,7 @@ c-parser EOF echo "Rearranging directories" -/bin/mv -v "$outputdir/src/tools/c-parser/README" "$outputdir" +/bin/mv -v "$outputdir/src/tools/c-parser/README.md" "$outputdir" /bin/mv -v "$outputdir/src/tools/c-parser" "$outputdir/src/" rmdir "$outputdir/src/tools"