Commit d1956f8e authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files

Fixed the README.md, including mini tutorial.

parent 491227fb
Pipeline #35046 passed with stage
in 15 minutes and 17 seconds
This diff is collapsed.
#!/bin/bash
REFINEDC_PATH="$( builtin cd "$( dirname "${BASH_SOURCE[0]}" )/.." >/dev/null 2>&1 && pwd )"
eval "$(builtin cd "${REFINEDC_PATH}" && opam env)"
# Check if Cerberus needs to be compiled (not enough to just exec here).
if [ ! -d "${REFINEDC_PATH}/_build" ]; then
echo -n "Compiling [rcgen]... "
dune build --no-print-directory --root "${REFINEDC_PATH}" 2> /dev/null ||
( echo "Error..." && return 1 )
echo "Done."
fi
# We forward the arguments to the actual command.
dune exec --no-print-directory --root "${REFINEDC_PATH}" -- rcgen "$@"
#!/bin/bash
set -e
REFINEDC_PATH="$( builtin cd "$( dirname "${BASH_SOURCE[0]}" )/.." >/dev/null 2>&1 && pwd )"
eval "$(builtin cd "${REFINEDC_PATH}" && opam env)"
### FEATURE DETECTION
MAKE_OPTIONS=""
# output sync is not available on old versions of make which come with macos
if make phony --output-sync >/dev/null 2>/dev/null; then
MAKE_OPTIONS="--output-sync"
fi
# linux
if command -v nproc >/dev/null 2>/dev/null; then
NPROC="${NPROC:-$(nproc)}"
fi
# macos
if [[ "x$(uname -s)" == "xDarwin" ]]; then
NPROC="${NPROC:-$(sysctl -n hw.logicalcpu)}"
fi
NPROC="${NPROC:-4}"
### ACTUAL BUILD CODE
function call_make () {
TIMED=y make $MAKE_OPTIONS --no-print-directory -k -j "$NPROC" "$@"
}
if [ "$#" -ne 1 ]; then
echo "Usage: $0 <C source file>"
exit 1
fi
if [[ "${1##*.}" == "c" ]]; then
# Compute the path to the source file, relative to the RefinedC root.
SRC=$(realpath --relative-to="${REFINEDC_PATH}" "$1")
SRC_NO_EXT="${SRC%.*}"
# Move to the refinedC root.
builtin cd "${REFINEDC_PATH}" || exit 1
# Generate code and rebuild the _CoqProject file.
./scripts/rcgen "${SRC}"
# Compute the .vo files that need to be built after generation.
TARGETS="${SRC_NO_EXT}_code.vo ${SRC_NO_EXT}_spec.vo"
for TARGET in "${SRC_NO_EXT}"_proof*.v; do
TARGETS="${TARGETS} ${TARGET}o"
done
make -B Makefile.coq
# Forward the targets to Coq makefile direclty (wrong deps otherwise).
call_make -f Makefile.coq $TARGETS
else
echo "Invalid extension on the argument (expecting a C file)."
exit 1
fi
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment