dune generate unsorted All.v

To fix composed builds, cf #201

Author: SkySkimmer

theories/All.sh

@@ -3,6 +3,13 @@ set -e
 set -u
 set -o pipefail
 cd "$(dirname "$0")"
+
 printf 'Set Warnings "-deprecated-library-file,-warn-library-file,-notation-incompatible-prefix,-notation-overridden,-overwriting-delimiting-key".\n'
-find . -regex '.*/[^.][^/]*[.]v' ! -path ./All.v | sort | xargs rocq dep -Q . Stdlib -sort | \
+
+if [ "$1" = "-unsorted" ]; then
+  rocqdep=xargs echo
+else
+  rocqdep="xargs rocq dep -Q . Stdlib -sort"
+fi
+find . -regex '.*/[^.][^/]*[.]v' ! -path ./All.v | sort | $rocqdep | \
   sed -e 's#\./#From Stdlib Require Export #g' -e 's#\.v\s*#.\n#g' -e 's#/#.#g'

theories/dune

@@ -12,4 +12,6 @@
 (rule
  (targets All.v)
  (deps All.sh (source_tree .))
- (action (with-stdout-to %{targets} (run env bash ./All.sh))))
+ ; -unsorted: coqdep will want the .vo for the corelib to be present
+ ; we could depend on rocq-core instead
+ (action (with-stdout-to %{targets} (run env bash ./All.sh -unsorted))))