Commit de4583d1 authored by Michael Sammler's avatar Michael Sammler
Browse files

Merge branch 'master' of gitlab.mpi-sws.org:iris/refinedc

parents 426b4baf 3ffe3d67
Pipeline #35422 failed with stage
in 2 minutes and 6 seconds
_build/
.merlin
*.vo
*.vos
*.vok
*.vio
*.v.d
.coqdeps.d
*.glob
*.cache
*.aux
\#*\#
.\#*
*~
......
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