compat coq 8.14 + core target (avoids building case studies).

Makefile.local

@@ -26,5 +26,10 @@ vok-nocheck: $(VOKFILESNOASSUMPTION)
 # specified in _coqProject because spaces in args are not supported by
 # coq_makefile.
 # Remove to see where we should add "Proof using annotations".
-COQEXTRAFLAGS+= -set "Suggest Proof Using=true"
+COQEXTRAFLAGS+= -set "Suggest Proof Using=yes"
 
+core: Pactole_all.vo
+
+recore:
+	dev/rebuild_pactole_all.sh > Pactole_all.v
+	make Pactole_all.vo

Pactole_all.v

+Require Import Pactole.Models.NoByzantine.
+Require Import Pactole.Models.RigidFlexibleEquivalence.
+Require Import Pactole.Models.ContinuousGraph.
+Require Import Pactole.Models.Rigid.
+Require Import Pactole.Models.RigidFlexibleEquivalence_Assumptions.
+Require Import Pactole.Models.DiscreteGraph.
+Require Import Pactole.Models.GraphEquivalence.
+Require Import Pactole.Models.Flexible.
+Require Import Pactole.Models.Similarity.
+Require Import Pactole.Spaces.Isomorphism.
+Require Import Pactole.Spaces.R.
+Require Import Pactole.Spaces.Ring.
+Require Import Pactole.Spaces.RealNormedSpace.
+Require Import Pactole.Spaces.RealMetricSpace.
+Require Import Pactole.Spaces.RealVectorSpace.
+Require Import Pactole.Spaces.EuclideanSpace.
+Require Import Pactole.Spaces.Grid.
+Require Import Pactole.Spaces.Similarity.
+Require Import Pactole.Spaces.Graph.
+Require Import Pactole.Spaces.R2.
+Require Import Pactole.Setting.
+Require Import Pactole.Observations.Definition.
+Require Import Pactole.Observations.MultisetObservation.
+Require Import Pactole.Observations.LimitedMultisetObservation.
+Require Import Pactole.Observations.PreCompositionObservation.
+Require Import Pactole.Observations.SetObservation.
+Require Import Pactole.Observations.PointedObservation.
+Require Import Pactole.Observations.LimitedSetObservation.
+Require Import Pactole.minipactole.minipactole.
+Require Import Pactole.Core.State.
+Require Import Pactole.Core.Configuration.
+Require Import Pactole.Core.Formalism.
+Require Import Pactole.Core.Identifiers.
+Require Import Pactole.Util.NumberComplements.
+Require Import Pactole.Util.ListComplements.
+Require Import Pactole.Util.SetoidDefs.
+Require Import Pactole.Util.Lexprod.
+Require Import Pactole.Util.FSets.FSetList.
+Require Import Pactole.Util.FSets.FSetInterface.
+Require Import Pactole.Util.FSets.FSetFacts.
+Require Import Pactole.Util.Bijection.
+Require Import Pactole.Util.FMaps.FMapInterface.
+Require Import Pactole.Util.FMaps.FMapList.
+Require Import Pactole.Util.FMaps.FMapFacts.
+Require Import Pactole.Util.Coqlib.
+Require Import Pactole.Util.Stream.
+Require Import Pactole.Util.MMultiset.MMultisetWMap.
+Require Import Pactole.Util.MMultiset.MMultisetFacts.
+Require Import Pactole.Util.MMultiset.MMultisetInterface.
+Require Import Pactole.Util.MMultiset.MMultisetExtraOps.
+Require Import Pactole.Util.MMultiset.Preliminary.
+Require Import Pactole.Util.Ratio.
+Require Import Pactole.Util.Preliminary.

_CoqProject

@@ -13,6 +13,10 @@
 #-arg -set
 #-arg "Suggest Proof Using=true"
 
+## All dependencies that are not case studies
+## Typically this should be the target of opam package
+Pactole_all.v
+
 ## External libraries
 #Util/FSets/OrderedType.v
 Util/FSets/FSetInterface.v

dev/depgraph.sh

+#!/bin/bash
+
+OPT="-Q . Pactole"
+VFILES=$(grep "^[^#].*\.v" _CoqProject)
+
+( echo "digraph interval_deps {" ;
+  echo "node [shape=ellipse, style=filled, URL=\"html/Interval.\N.html\", color=black];";
+  ( coqdep $OPT $VFILES ) |
+    sed -n -e 's,/,.,g;s/[.]vo.*: [^ ]*[.]v//p' |
+    while read src dst; do
+      color=$(echo "$src" | sed -e 's,Real.*,turquoise,;s,Interval[.].*,plum,;s,Integral.*,lightcoral,;s,Poly.*,yellow,;s,Float.*,cornflowerblue,;s,Eval.*,green,;s,[A-Z].*,white,')
+      echo "\"$src\" [fillcolor=$color];"
+      for d in $dst; do
+        echo "\"$src\" -> \"${d%.vo}\" ;"
+      done
+    done;
+  echo "}" ) | tred > deps.dot
+dot -T png deps.dot > deps.png
+dot -T cmap deps.dot | sed -e 's,>$,/>,' > deps.map

dev/rebuild_pactole_all.sh

+
+
+
+
+TOLERATED="Pactole_all.v\\|Util/FSets/OrderedType.v\\|CaseStudies/Volumes/NoCollisionAndPath.v"
+VFILES=$(find . -name "*.v" | sed -e 's/\.\///' | grep -v "\.#\\|*~" | grep -v $TOLERATED | grep -v CaseStudies)
+
+for i in $VFILES ; do
+    echo $i | sed -e 's/\.v/./' | sed -e 's/\//./g' | sed -e 's/^/Require Import Pactole./'
+done