From 525c94c8ae33fbea71a4a4400fffc0bec0fc3564 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Thu, 7 Nov 2019 13:45:39 +0100
Subject: [PATCH] create_makefile.sh: support --without-classic

It's faster to just compile the new stuff. For new developments,
that's sufficient.
---
 README.md          |  6 ++++++
 create_makefile.sh | 21 ++++++++++++++++++++-
 2 files changed, 26 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 0c90f604e..435f995f2 100644
--- a/README.md
+++ b/README.md
@@ -34,6 +34,12 @@ First, create an appropriate `Makefile`.
 ./create_makefile.sh
 ```
 
+Alternatively, to avoid compiling the older "classic" Prosa, specify the `--without-classic` option.
+
+```
+./create_makefile.sh --without-classic
+```
+
 Second, compile the library.
 
 ```
diff --git a/create_makefile.sh b/create_makefile.sh
index 95eba0429..46c35de0c 100755
--- a/create_makefile.sh
+++ b/create_makefile.sh
@@ -1,11 +1,30 @@
 #!/bin/bash 
 
+while ! [ -z "$1" ]
+do
+    case "$1" in
+        --without-classic)
+            SKIP_CLASSIC=yes
+            ;;
+        *)
+            echo "Unrecognized option: $1"
+            exit 1
+            ;;
+    esac
+    shift
+done
+
 # Include rt-proofs library in _CoqProject.
 # (For Coq versions >= 8.6, remove spurious warnings.)
 echo -R . rt -arg \"-w -notation-overriden,-parsing\" > _CoqProject
 
 # Compile all *.v files
-coq_makefile -f _CoqProject $(find . -name "*.v"  ! -name "*#*" ! -path "./.git/*" -print) -o Makefile
+if [ "yes" == "$SKIP_CLASSIC" ]
+then
+    coq_makefile -f _CoqProject $(find . -name "*.v"  ! -name "*#*" ! -path "./.git/*" ! -path "./classic/*" -print) -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
 # and cause clashes for files with the same name. This forces full filenames and
-- 
GitLab