From 88748cdbea1609de367a1e034606207d66b70508 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 20 Dec 2000 15:23:08 +0000 Subject: [PATCH] Initial --- helm/EXPORT/export_Marseille_CCS/Makefile | 11 +++++++ .../export_Marseille_CCS/exporttheories.sh | 10 ++++++ .../prova_Marseille_CCS.v | 5 +++ helm/EXPORT/export_Nijmegen_Rem/Makefile | 11 +++++++ .../export_Nijmegen_Rem/exporttheories.sh | 10 ++++++ .../export_Nijmegen_Rem/prova_Nijmegen_Rem.v | 5 +++ helm/EXPORT/export_Paris_ZF/Makefile | 25 ++++++++++++++ helm/EXPORT/export_Paris_ZF/exporttheories.sh | 10 ++++++ helm/EXPORT/export_Paris_ZF/prova_Paris_ZF.v | 33 +++++++++++++++++++ helm/EXPORT/export_Rocq_CHECKER/Makefile | 11 +++++++ .../export_Rocq_CHECKER/exporttheories.sh | 10 ++++++ .../export_Rocq_CHECKER/prova_Rocq_CHECKER.v | 7 ++++ helm/EXPORT/export_Rocq_SHUFFLE/Makefile | 16 +++++++++ .../export_Rocq_SHUFFLE/exporttheories.sh | 10 ++++++ .../export_Rocq_SHUFFLE/prova_Rocq_SHUFFLE.v | 16 +++++++++ 15 files changed, 190 insertions(+) create mode 100644 helm/EXPORT/export_Marseille_CCS/Makefile create mode 100755 helm/EXPORT/export_Marseille_CCS/exporttheories.sh create mode 100644 helm/EXPORT/export_Marseille_CCS/prova_Marseille_CCS.v create mode 100644 helm/EXPORT/export_Nijmegen_Rem/Makefile create mode 100755 helm/EXPORT/export_Nijmegen_Rem/exporttheories.sh create mode 100644 helm/EXPORT/export_Nijmegen_Rem/prova_Nijmegen_Rem.v create mode 100644 helm/EXPORT/export_Paris_ZF/Makefile create mode 100755 helm/EXPORT/export_Paris_ZF/exporttheories.sh create mode 100644 helm/EXPORT/export_Paris_ZF/prova_Paris_ZF.v create mode 100644 helm/EXPORT/export_Rocq_CHECKER/Makefile create mode 100755 helm/EXPORT/export_Rocq_CHECKER/exporttheories.sh create mode 100644 helm/EXPORT/export_Rocq_CHECKER/prova_Rocq_CHECKER.v create mode 100644 helm/EXPORT/export_Rocq_SHUFFLE/Makefile create mode 100755 helm/EXPORT/export_Rocq_SHUFFLE/exporttheories.sh create mode 100644 helm/EXPORT/export_Rocq_SHUFFLE/prova_Rocq_SHUFFLE.v diff --git a/helm/EXPORT/export_Marseille_CCS/Makefile b/helm/EXPORT/export_Marseille_CCS/Makefile new file mode 100644 index 000000000..7c30db4a5 --- /dev/null +++ b/helm/EXPORT/export_Marseille_CCS/Makefile @@ -0,0 +1,11 @@ +all: objects theories + +objects: + coqc -R CCS Marseille.CCS CCS/*.v + echo "Load Verbose prova_Marseille_CCS." | coqtop.byte -R CCS Marseille.CCS + +theories: + ./exporttheories.sh + +clean: + rm -f *.vo CCS/*.vo diff --git a/helm/EXPORT/export_Marseille_CCS/exporttheories.sh b/helm/EXPORT/export_Marseille_CCS/exporttheories.sh new file mode 100755 index 000000000..24fce6c39 --- /dev/null +++ b/helm/EXPORT/export_Marseille_CCS/exporttheories.sh @@ -0,0 +1,10 @@ +#!/bin/bash + +echo "Exporting theory $1"; + +for i in CCS/*.v + do + basename=$(basename $i | sed s/\\.v//) + cat $i | ../mktheory.pl "Marseille/CCS/$basename" > \ + examples/Marseille/CCS/$basename.theory.xml + done diff --git a/helm/EXPORT/export_Marseille_CCS/prova_Marseille_CCS.v b/helm/EXPORT/export_Marseille_CCS/prova_Marseille_CCS.v new file mode 100644 index 000000000..e44066736 --- /dev/null +++ b/helm/EXPORT/export_Marseille_CCS/prova_Marseille_CCS.v @@ -0,0 +1,5 @@ +Require Export Xml. + +Require Trans_Sys. + +Print XML Module Disk "examples" Trans_Sys. diff --git a/helm/EXPORT/export_Nijmegen_Rem/Makefile b/helm/EXPORT/export_Nijmegen_Rem/Makefile new file mode 100644 index 000000000..3421cc0a6 --- /dev/null +++ b/helm/EXPORT/export_Nijmegen_Rem/Makefile @@ -0,0 +1,11 @@ +all: objects theories + +objects: + coqc -R Rem Nijmegen.Rem Rem/*.v + echo "Load Verbose prova_Nijmegen_Rem." | coqtop.byte -R Rem Nijmegen.Rem + +theories: + ./exporttheories.sh + +clean: + rm -f *.vo Rem/*.vo diff --git a/helm/EXPORT/export_Nijmegen_Rem/exporttheories.sh b/helm/EXPORT/export_Nijmegen_Rem/exporttheories.sh new file mode 100755 index 000000000..8e64b90c5 --- /dev/null +++ b/helm/EXPORT/export_Nijmegen_Rem/exporttheories.sh @@ -0,0 +1,10 @@ +#!/bin/bash + +echo "Exporting theory $1"; + +for i in Rem/*.v + do + basename=$(basename $i | sed s/\\.v//) + cat $i | ../mktheory.pl "Nijmegen/Rem/$basename" > \ + examples/Nijmegen/Rem/$basename.theory.xml + done diff --git a/helm/EXPORT/export_Nijmegen_Rem/prova_Nijmegen_Rem.v b/helm/EXPORT/export_Nijmegen_Rem/prova_Nijmegen_Rem.v new file mode 100644 index 000000000..04244aa30 --- /dev/null +++ b/helm/EXPORT/export_Nijmegen_Rem/prova_Nijmegen_Rem.v @@ -0,0 +1,5 @@ +Require Export Xml. + +Require Rem. + +Print XML Module Disk "examples" Rem. diff --git a/helm/EXPORT/export_Paris_ZF/Makefile b/helm/EXPORT/export_Paris_ZF/Makefile new file mode 100644 index 000000000..ee2f95e1b --- /dev/null +++ b/helm/EXPORT/export_Paris_ZF/Makefile @@ -0,0 +1,25 @@ +all: objects theories + +objects: + coqc -R ZF/src Paris.ZF ZF/src/nothing.v + coqc -R ZF/src Paris.ZF ZF/src/useful.v + coqc -R ZF/src Paris.ZF ZF/src/ZFbasis.v + coqc -R ZF/src Paris.ZF ZF/src/axs_extensionnalite.v + coqc -R ZF/src Paris.ZF ZF/src/axs_paire.v + coqc -R ZF/src Paris.ZF ZF/src/axs_reunion.v + coqc -R ZF/src Paris.ZF ZF/src/axs_parties.v + coqc -R ZF/src Paris.ZF ZF/src/axs_comprehension.v + coqc -R ZF/src Paris.ZF ZF/src/axs_remplacement.v + coqc -R ZF/src Paris.ZF ZF/src/couples.v + coqc -R ZF/src Paris.ZF ZF/src/applications.v + coqc -R ZF/src Paris.ZF ZF/src/axs_choice.v + coqc -R ZF/src Paris.ZF ZF/src/axs_fundation.v + coqc -R ZF/src Paris.ZF ZF/src/ZFrelations.v + coqc -R ZF/src Paris.ZF ZF/src/MSetBasis.v + echo "Load Verbose prova_Paris_ZF." | coqtop.byte -R ZF/src Paris.ZF + +theories: + ./exporttheories.sh + +clean: + rm -f *.vo ZF/src/*.vo diff --git a/helm/EXPORT/export_Paris_ZF/exporttheories.sh b/helm/EXPORT/export_Paris_ZF/exporttheories.sh new file mode 100755 index 000000000..3a0db3d49 --- /dev/null +++ b/helm/EXPORT/export_Paris_ZF/exporttheories.sh @@ -0,0 +1,10 @@ +#!/bin/bash + +echo "Exporting theory $1"; + +for i in ZF/src/*.v + do + basename=$(basename $i | sed s/\\.v//) + cat $i | ../mktheory.pl "Paris/ZF/$basename" > \ + examples/Paris/ZF/$basename.theory.xml + done diff --git a/helm/EXPORT/export_Paris_ZF/prova_Paris_ZF.v b/helm/EXPORT/export_Paris_ZF/prova_Paris_ZF.v new file mode 100644 index 000000000..03f59427f --- /dev/null +++ b/helm/EXPORT/export_Paris_ZF/prova_Paris_ZF.v @@ -0,0 +1,33 @@ +Require Export Xml. + +Require nothing. +Require useful. +Require ZFbasis. +Require axs_extensionnalite. +Require axs_paire . +Require axs_reunion. +Require axs_parties. +Require axs_comprehension. +Require axs_remplacement. +Require couples. +Require applications . +Require axs_choice. +Require axs_fundation. +Require ZFrelations. +Require MSetBasis . + +Print XML Module Disk "examples" nothing. +Print XML Module Disk "examples" useful. +Print XML Module Disk "examples" ZFbasis. +Print XML Module Disk "examples" axs_extensionnalite. +Print XML Module Disk "examples" axs_paire . +Print XML Module Disk "examples" axs_reunion. +Print XML Module Disk "examples" axs_parties. +Print XML Module Disk "examples" axs_comprehension. +Print XML Module Disk "examples" axs_remplacement. +Print XML Module Disk "examples" couples. +Print XML Module Disk "examples" applications . +Print XML Module Disk "examples" axs_choice. +Print XML Module Disk "examples" axs_fundation. +Print XML Module Disk "examples" ZFrelations. +Print XML Module Disk "examples" MSetBasis . diff --git a/helm/EXPORT/export_Rocq_CHECKER/Makefile b/helm/EXPORT/export_Rocq_CHECKER/Makefile new file mode 100644 index 000000000..76fe9308a --- /dev/null +++ b/helm/EXPORT/export_Rocq_CHECKER/Makefile @@ -0,0 +1,11 @@ +all: objects theories + +objects: + coqc -R CHECKER Rocq.CHECKER CHECKER/Functions.v CHECKER/Checker.v + echo "Load Verbose prova_Rocq_CHECKER." | coqtop.byte -R CHECKER Rocq.CHECKER + +theories: + ./exporttheories.sh + +clean: + rm -f *.vo CHECKER/*.vo diff --git a/helm/EXPORT/export_Rocq_CHECKER/exporttheories.sh b/helm/EXPORT/export_Rocq_CHECKER/exporttheories.sh new file mode 100755 index 000000000..e0152041f --- /dev/null +++ b/helm/EXPORT/export_Rocq_CHECKER/exporttheories.sh @@ -0,0 +1,10 @@ +#!/bin/bash + +echo "Exporting theory $1"; + +for i in CHECKER/*.v + do + basename=$(basename $i | sed s/\\.v//) + cat $i | ../mktheory.pl "Rocq/CHECKER/$basename" > \ + examples/Rocq/CHECKER/$basename.theory.xml + done diff --git a/helm/EXPORT/export_Rocq_CHECKER/prova_Rocq_CHECKER.v b/helm/EXPORT/export_Rocq_CHECKER/prova_Rocq_CHECKER.v new file mode 100644 index 000000000..190588474 --- /dev/null +++ b/helm/EXPORT/export_Rocq_CHECKER/prova_Rocq_CHECKER.v @@ -0,0 +1,7 @@ +Require Export Xml. + +Require Functions. +Require Checker. + +Print XML Module Disk "examples" Functions. +Print XML Module Disk "examples" Checker. diff --git a/helm/EXPORT/export_Rocq_SHUFFLE/Makefile b/helm/EXPORT/export_Rocq_SHUFFLE/Makefile new file mode 100644 index 000000000..ba2ab5712 --- /dev/null +++ b/helm/EXPORT/export_Rocq_SHUFFLE/Makefile @@ -0,0 +1,16 @@ +all: objects theories + +objects: + coqc -R SHUFFLE Rocq.SHUFFLE SHUFFLE/Words.v + coqc -R SHUFFLE Rocq.SHUFFLE SHUFFLE/Alternate.v + coqc -R SHUFFLE Rocq.SHUFFLE SHUFFLE/Opposite.v + coqc -R SHUFFLE Rocq.SHUFFLE SHUFFLE/Paired.v + coqc -R SHUFFLE Rocq.SHUFFLE SHUFFLE/Shuffle.v + coqc -R SHUFFLE Rocq.SHUFFLE SHUFFLE/Gilbreath.v + echo "Load Verbose prova_Rocq_SHUFFLE." | coqtop.byte -R SHUFFLE Rocq.SHUFFLE + +theories: + ./exporttheories.sh + +clean: + rm -f *.vo SHUFFLE/*.vo diff --git a/helm/EXPORT/export_Rocq_SHUFFLE/exporttheories.sh b/helm/EXPORT/export_Rocq_SHUFFLE/exporttheories.sh new file mode 100755 index 000000000..acd865a42 --- /dev/null +++ b/helm/EXPORT/export_Rocq_SHUFFLE/exporttheories.sh @@ -0,0 +1,10 @@ +#!/bin/bash + +echo "Exporting theory $1"; + +for i in SHUFFLE/*.v + do + basename=$(basename $i | sed s/\\.v//) + cat $i | ../mktheory.pl "Rocq/SHUFFLE/$basename" > \ + examples/Rocq/SHUFFLE/$basename.theory.xml + done diff --git a/helm/EXPORT/export_Rocq_SHUFFLE/prova_Rocq_SHUFFLE.v b/helm/EXPORT/export_Rocq_SHUFFLE/prova_Rocq_SHUFFLE.v new file mode 100644 index 000000000..1b17a93bc --- /dev/null +++ b/helm/EXPORT/export_Rocq_SHUFFLE/prova_Rocq_SHUFFLE.v @@ -0,0 +1,16 @@ +Require Export Xml. + +Require Alternate. +Require Gilbreath. +Require Opposite. +Require Paired. +Require Shuffle. +Require Words. + + +Print XML Module Disk "examples" Alternate. +Print XML Module Disk "examples" Gilbreath. +Print XML Module Disk "examples" Opposite. +Print XML Module Disk "examples" Paired. +Print XML Module Disk "examples" Shuffle. +Print XML Module Disk "examples" Words. -- 2.39.2