File: make-library-files

package info (click to toggle)
coq-doc 8.4pl4-2
  • links: PTS, VCS
  • area: non-free
  • in suites: stretch
  • size: 21,852 kB
  • ctags: 24,335
  • sloc: ml: 140,953; ansic: 1,982; lisp: 1,406; sh: 1,347; makefile: 572; sed: 2
file content (36 lines) | stat: -rwxr-xr-x 1,249 bytes parent folder | download | duplicates (3)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
#!/bin/sh

# Needs COQSRC and GALLINA set

# On garde la liste de tous les *.v avec dates dans library.files.ls
# Si elle a change depuis la derniere fois ou library.files n'existe pas
# on fabrique des .g (si besoin) et la liste library.files dans 
# l'ordre de ls -tr des *.vo
# Ce dernier trie les fichiers dans l'ordre inverse de leur date de cration
# En supposant que make fait son boulot, ca fait un tri topologique du
# graphe des dpendances

LIBDIRS="Arith PArith NArith ZArith Reals Logic Bool Lists Relations Sets Sorting Wellfounded Setoids Program Classes Numbers"

rm -f library.files.ls.tmp
(cd $COQSRC/theories; find $LIBDIR -name "*.v" -ls) > library.files.ls.tmp
if ! test -e library.files || ! cmp library.files.ls library.files.ls.tmp; then
  mv -f library.files.ls.tmp library.files.ls
  rm -f library.files; touch library.files
  ABSOLUTE=`pwd`/library.files
  cd $COQSRC/theories
  echo $LIBDIRS
  for rep in $LIBDIRS ; do
    (cd $rep
     echo $rep/intro.tex >> $ABSOLUTE
     VOFILES=`ls -tr *.vo`
     for file in $VOFILES ; do
       VF=`basename $file \.vo`
       if [ \( ! -e $VF.g \) -o \( $VF.v -nt $VF.g \) ] ; then
          $GALLINA $VF.v
       fi
       echo $rep/$VF.g >> $ABSOLUTE
     done
    )
  done
fi