1- #! /bin/bash
1+ #! /usr/ bin/env bash
22
33# ## coqproject.sh
44# ## Creates a _CoqProject file, including external dependencies.
55
6- # # Configuration options
7- # External dependencies
8- # e.g. DEPS = (StructTact)
6+ # ## See README.md for a description.
97
10- # Directories containing coq files
11- # e.g. DIRS=(theories)
12- if [ -z ${DIRS+x} ]; then DIRS=(.); fi
13-
14- # Canary imports, along with error messages if imports fail
15- # e.g. CANARIES=("mathcomp.ssreflect.ssreflect" "Ssreflect missing")
16-
17- # Namespaces corresponding to directories. By default, everything is in "".
18- # To put "theories" in the "FermatsTheorem" namespace:
19- # NAMESPACE_theories=FermatsTheorem
20- # Note that "." can't be part of a variable name, so it's replaced by "_".
21- # So, to put the current directory in the "FermatsTheorem" namespace:
22- # NAMESPACE__=FermatsTheorem
23-
24- # Extra files (e.g. automatically-generated .v files that won't be
25- # around at configure-time)
26- # e.g. EXTRA=(GeneratedFile.v)
278# # Implementation
289
10+ if [ -z ${DIRS+x} ]; then DIRS=(.); fi
11+
2912COQPROJECT_TMP=_CoqProject.tmp
3013
3114rm -f $COQPROJECT_TMP
3215touch $COQPROJECT_TMP
16+
17+ function dep_dirs_lines(){
18+ dep_dirs_var=" $2 " _DIRS
19+ local -a ' dep_dirs=("${' " $dep_dirs_var " ' [@]}")'
20+ if [ " x${dep_dirs[0]} " = " x" ]; then dep_dirs=(.); fi
21+ for dep_dir in " ${dep_dirs[@]} " ; do
22+ namespace_var=NAMESPACE_" $2 " _" $dep_dir "
23+ namespace_var=${namespace_var// \/ / _}
24+ namespace_var=${namespace_var// -/ _}
25+ namespace_var=${namespace_var// ./ _}
26+ namespace=${! namespace_var:= $2 }
27+ LINE=" -Q $1 /$dep_dir / $namespace "
28+ echo $LINE >> $COQPROJECT_TMP
29+ done
30+ }
3331for dep in ${DEPS[@]} ; do
3432 path_var=" $dep " _PATH
3533 path=${! path_var:= " ../$dep " }
@@ -42,8 +40,8 @@ for dep in ${DEPS[@]}; do
4240 path=$( pwd)
4341 popd > /dev/null
4442 echo " $dep found at $path "
45- LINE= " -Q $path $dep "
46- echo $LINE >> $COQPROJECT_TMP
43+
44+ dep_dirs_lines $path $dep
4745done
4846
4947COQTOP=" coqtop $( cat $COQPROJECT_TMP ) "
6260
6361for dir in ${DIRS[@]} ; do
6462 namespace_var=NAMESPACE_" $dir "
63+ namespace_var=${namespace_var// \/ / _}
64+ namespace_var=${namespace_var// -/ _}
6565 namespace_var=${namespace_var// ./ _}
6666 namespace=${! namespace_var:= " \"\" " }
67- LINE=" -Q $dir $namespace "
67+ LINE=" -Q $dir / $namespace "
6868 echo $LINE >> $COQPROJECT_TMP
6969done
7070
7171for dir in ${DIRS[@]} ; do
7272 echo >> $COQPROJECT_TMP
73- find $dir -iname ' *.v' >> $COQPROJECT_TMP
73+ find $dir -iname ' *.v' -not -name ' *\#* ' >> $COQPROJECT_TMP
7474done
7575
7676for extra in ${EXTRA[@]} ; do
0 commit comments