From 015781acfe4a2a75eeced513528b389cae9fb0a3 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 23 Feb 2006 14:21:14 +0000
Subject: Mise à jour des Makefile, ajout licences, corrections mineures suite
 à restructuration du répertoire de documentation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8607 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/stdlib/make-library-files | 36 ++++++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)
 create mode 100755 doc/stdlib/make-library-files

(limited to 'doc/stdlib/make-library-files')

diff --git a/doc/stdlib/make-library-files b/doc/stdlib/make-library-files
new file mode 100755
index 0000000000..91e3cc3f45
--- /dev/null
+++ b/doc/stdlib/make-library-files
@@ -0,0 +1,36 @@
+#!/bin/sh
+
+# Needs COQTOP 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 création
+# En supposant que make fait son boulot, ca fait un tri topologique du
+# graphe des dépendances
+
+LIBDIRS="Arith NArith ZArith Reals Logic Bool Lists IntMap Relations Sets Sorting Wellfounded Setoids"
+
+rm -f library.files.ls.tmp
+(cd $COQTOP/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 $COQTOP/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
-- 
cgit v1.2.3