Skip to content
Snippets Groups Projects
Commit 3b18aa36 authored by Björn Brandenburg's avatar Björn Brandenburg
Browse files

create_makefile.sh: add --only-classic option

Add support for compiling only classic Prosa, i.e., the inverse of
--without-classic.
parent 1dad4615
No related branches found
No related tags found
No related merge requests found
#!/bin/bash #!/bin/bash
# options passed to `find` for locating relevant source files
FIND_OPTS=( . -name '*.v' ! -name '*#*' ! -path './.git/*' )
while ! [ -z "$1" ] while ! [ -z "$1" ]
do do
case "$1" in case "$1" in
--without-classic) --without-classic)
SKIP_CLASSIC=yes FIND_OPTS+=( ! -path './classic/*' )
;;
--only-classic)
FIND_OPTS+=( ! -path './restructuring/*' )
;; ;;
*) *)
echo "Unrecognized option: $1" echo "Unrecognized option: $1"
...@@ -14,13 +20,10 @@ do ...@@ -14,13 +20,10 @@ do
shift shift
done done
# Compile all *.v files FIND_OPTS+=( -print )
if [ "yes" == "$SKIP_CLASSIC" ]
then # Compile all relevant *.v files
coq_makefile -f _CoqProject $(find . -name "*.v" ! -name "*#*" ! -path "./.git/*" ! -path "./classic/*" -print) -o Makefile coq_makefile -f _CoqProject $(find "${FIND_OPTS[@]}" ) -o Makefile
else
coq_makefile -f _CoqProject $(find . -name "*.v" ! -name "*#*" ! -path "./.git/*" -print) -o Makefile
fi
# Fix the 'make validate' command. It doesn't handle the library prefix properly # Fix the 'make validate' command. It doesn't handle the library prefix properly
# and cause clashes for files with the same name. This forces full filenames and # and cause clashes for files with the same name. This forces full filenames and
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment