diff --git a/.woodpecker/mk_release b/.woodpecker/mk_release index b470536..0b64102 100755 --- a/.woodpecker/mk_release +++ b/.woodpecker/mk_release @@ -83,18 +83,18 @@ build_and_install_manuals() if [ "$DIRTY" = "true" ]; then if [ -z ${ARTIFACT_DIR+x} ]; then echo " * Quick and Dirty Mode (local build)" - $ISABELLE build -d . Isabelle_DOF Isabelle_DOF-Example-Scholarly_Paper - mkdir -p $ISADOF_WORK_DIR/Isabelle_DOF-Example-Scholarly_Paper/output/ - cp Isabelle_DOF-Example-Scholarly_Paper/output/document.pdf \ - $ISADOF_WORK_DIR/Isabelle_DOF-Example-Scholarly_Paper/output/ + $ISABELLE build -d . Isabelle_DOF Isabelle_DOF-Example-I + mkdir -p $ISADOF_WORK_DIR/Isabelle_DOF-Example-I/output/ + cp Isabelle_DOF-Example-I/output/document.pdf \ + $ISADOF_WORK_DIR/Isabelle_DOF-Example-I/output/ mkdir -p $ISADOF_WORK_DIR/Isabelle_DOF/output/ cp Isabelle_DOF/output/document.pdf \ $ISADOF_WORK_DIR/Isabelle_DOF/output/; else echo " * Quick and Dirty Mode (running on CI)" - mkdir -p $ISADOF_WORK_DIR/Isabelle_DOF-Example-Scholarly_Paper/output/ - cp $ARTIFACT_DIR/browser_info/Unsorted/Isabelle_DOF-Example-Scholarly_Paper/document.pdf \ - $ISADOF_WORK_DIR/Isabelle_DOF-Example-Scholarly_Paper/output/ + mkdir -p $ISADOF_WORK_DIR/Isabelle_DOF-Example-I/output/ + cp $ARTIFACT_DIR/browser_info/Unsorted/Isabelle_DOF-Example-I/document.pdf \ + $ISADOF_WORK_DIR/Isabelle_DOF-Example-I/output/ mkdir -p $ISADOF_WORK_DIR/Isabelle_DOF/output/ cp $ARTIFACT_DIR/browser_info/Unsorted/Isabelle_DOF/document.pdf \ @@ -111,9 +111,9 @@ build_and_install_manuals() $ISADOF_WORK_DIR/doc/Isabelle_DOF-Manual.pdf echo " Isabelle_DOF-Manual User and Implementation Manual for Isabelle/DOF" >> $ISADOF_WORK_DIR/doc/Contents - cp $ISADOF_WORK_DIR/Isabelle_DOF-Example-Scholarly_Paper/output/document.pdf \ - $ISADOF_WORK_DIR/doc/Isabelle_DOF-Example-Scholarly_Paper.pdf - echo " Isabelle_DOF-Example-Scholarly_Paper Example academic paper" >> $ISADOF_WORK_DIR/doc/Contents + cp $ISADOF_WORK_DIR/Isabelle_DOF-Example-I/output/document.pdf \ + $ISADOF_WORK_DIR/doc/Isabelle_DOF-Example-I.pdf + echo " Isabelle_DOF-Example-I Example academic paper" >> $ISADOF_WORK_DIR/doc/Contents find $ISADOF_WORK_DIR -type d -name "output" -exec rm -rf {} \; &> /dev/null || true rm -rf $ISADOF_WORK_DIR/.git* $ISADOF_WORK_DIR/.woodpecker $ISADOF_WORK_DIR/.afp diff --git a/Isabelle_DOF-Example-I/ROOT b/Isabelle_DOF-Example-I/ROOT index ba9c4e4..21a9c2c 100644 --- a/Isabelle_DOF-Example-I/ROOT +++ b/Isabelle_DOF-Example-I/ROOT @@ -1,4 +1,4 @@ -session "2018-CICM-Linking" (AFP) = "Isabelle_DOF" + +session "Isabelle_DOF-Example-I" (AFP) = "Isabelle_DOF" + options [document = pdf, document_output = "output", document_build = dof] theories IsaDofApplications diff --git a/Isabelle_DOF-Example-II/ROOT b/Isabelle_DOF-Example-II/ROOT index 8e68278..28d1998 100644 --- a/Isabelle_DOF-Example-II/ROOT +++ b/Isabelle_DOF-Example-II/ROOT @@ -1,4 +1,4 @@ -session "2020-iFM-csp" = "Isabelle_DOF" + +session "Isabelle_DOF-Example-II" = "Isabelle_DOF" + options [document = pdf, document_output = "output", document_build = dof] theories "paper" diff --git a/Isabelle_DOF-Example-Extra/CC_ISO15408/PikeOS_study/PikeOS_ST.thy b/Isabelle_DOF-Examples-Extra/CC_ISO15408/PikeOS_study/PikeOS_ST.thy similarity index 100% rename from Isabelle_DOF-Example-Extra/CC_ISO15408/PikeOS_study/PikeOS_ST.thy rename to Isabelle_DOF-Examples-Extra/CC_ISO15408/PikeOS_study/PikeOS_ST.thy diff --git a/Isabelle_DOF-Example-Extra/CC_ISO15408/PikeOS_study/ROOT b/Isabelle_DOF-Examples-Extra/CC_ISO15408/PikeOS_study/ROOT similarity index 100% rename from Isabelle_DOF-Example-Extra/CC_ISO15408/PikeOS_study/ROOT rename to Isabelle_DOF-Examples-Extra/CC_ISO15408/PikeOS_study/ROOT diff --git a/Isabelle_DOF-Example-Extra/CC_ISO15408/ROOTS b/Isabelle_DOF-Examples-Extra/CC_ISO15408/ROOTS similarity index 100% rename from Isabelle_DOF-Example-Extra/CC_ISO15408/ROOTS rename to Isabelle_DOF-Examples-Extra/CC_ISO15408/ROOTS diff --git a/Isabelle_DOF-Example-Extra/CENELEC_50128/ROOTS b/Isabelle_DOF-Examples-Extra/CENELEC_50128/ROOTS similarity index 100% rename from Isabelle_DOF-Example-Extra/CENELEC_50128/ROOTS rename to Isabelle_DOF-Examples-Extra/CENELEC_50128/ROOTS diff --git a/Isabelle_DOF-Example-Extra/CENELEC_50128/mini_odo/ROOT b/Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/ROOT similarity index 100% rename from Isabelle_DOF-Example-Extra/CENELEC_50128/mini_odo/ROOT rename to Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/ROOT diff --git a/Isabelle_DOF-Example-Extra/CENELEC_50128/mini_odo/document/figures/df-numerics-encshaft.png b/Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/document/figures/df-numerics-encshaft.png similarity index 100% rename from Isabelle_DOF-Example-Extra/CENELEC_50128/mini_odo/document/figures/df-numerics-encshaft.png rename to Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/document/figures/df-numerics-encshaft.png diff --git a/Isabelle_DOF-Example-Extra/CENELEC_50128/mini_odo/document/figures/odometer.jpeg b/Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/document/figures/odometer.jpeg similarity index 100% rename from Isabelle_DOF-Example-Extra/CENELEC_50128/mini_odo/document/figures/odometer.jpeg rename to Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/document/figures/odometer.jpeg diff --git a/Isabelle_DOF-Example-Extra/CENELEC_50128/mini_odo/document/figures/three-phase-odo.pdf b/Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/document/figures/three-phase-odo.pdf similarity index 100% rename from Isabelle_DOF-Example-Extra/CENELEC_50128/mini_odo/document/figures/three-phase-odo.pdf rename to Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/document/figures/three-phase-odo.pdf diff --git a/Isabelle_DOF-Example-Extra/CENELEC_50128/mini_odo/document/figures/wheel-df.png b/Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/document/figures/wheel-df.png similarity index 100% rename from Isabelle_DOF-Example-Extra/CENELEC_50128/mini_odo/document/figures/wheel-df.png rename to Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/document/figures/wheel-df.png diff --git a/Isabelle_DOF-Example-Extra/CENELEC_50128/mini_odo/document/lstisadof.sty b/Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/document/lstisadof.sty similarity index 100% rename from Isabelle_DOF-Example-Extra/CENELEC_50128/mini_odo/document/lstisadof.sty rename to Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/document/lstisadof.sty diff --git a/Isabelle_DOF-Example-Extra/CENELEC_50128/mini_odo/document/preamble.tex b/Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/document/preamble.tex similarity index 100% rename from Isabelle_DOF-Example-Extra/CENELEC_50128/mini_odo/document/preamble.tex rename to Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/document/preamble.tex diff --git a/Isabelle_DOF-Example-Extra/CENELEC_50128/mini_odo/document/root.bib b/Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/document/root.bib similarity index 100% rename from Isabelle_DOF-Example-Extra/CENELEC_50128/mini_odo/document/root.bib rename to Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/document/root.bib diff --git a/Isabelle_DOF-Example-Extra/CENELEC_50128/mini_odo/document/root.mst b/Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/document/root.mst similarity index 100% rename from Isabelle_DOF-Example-Extra/CENELEC_50128/mini_odo/document/root.mst rename to Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/document/root.mst diff --git a/Isabelle_DOF-Example-Extra/CENELEC_50128/mini_odo/mini_odo.thy b/Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/mini_odo.thy similarity index 100% rename from Isabelle_DOF-Example-Extra/CENELEC_50128/mini_odo/mini_odo.thy rename to Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/mini_odo.thy diff --git a/Isabelle_DOF-Example-Extra/README.md b/Isabelle_DOF-Examples-Extra/README.md similarity index 100% rename from Isabelle_DOF-Example-Extra/README.md rename to Isabelle_DOF-Examples-Extra/README.md diff --git a/Isabelle_DOF-Example-Extra/ROOTS b/Isabelle_DOF-Examples-Extra/ROOTS similarity index 100% rename from Isabelle_DOF-Example-Extra/ROOTS rename to Isabelle_DOF-Examples-Extra/ROOTS diff --git a/Isabelle_DOF-Example-Extra/cytology/Cytology.thy b/Isabelle_DOF-Examples-Extra/cytology/Cytology.thy similarity index 100% rename from Isabelle_DOF-Example-Extra/cytology/Cytology.thy rename to Isabelle_DOF-Examples-Extra/cytology/Cytology.thy diff --git a/Isabelle_DOF-Example-Extra/cytology/ROOT b/Isabelle_DOF-Examples-Extra/cytology/ROOT similarity index 100% rename from Isabelle_DOF-Example-Extra/cytology/ROOT rename to Isabelle_DOF-Examples-Extra/cytology/ROOT diff --git a/Isabelle_DOF-Example-Extra/technical_report/ROOTS b/Isabelle_DOF-Examples-Extra/technical_report/ROOTS similarity index 100% rename from Isabelle_DOF-Example-Extra/technical_report/ROOTS rename to Isabelle_DOF-Examples-Extra/technical_report/ROOTS diff --git a/Isabelle_DOF-Example-Extra/technical_report/TR_my_commented_isabelle/ROOT b/Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/ROOT similarity index 100% rename from Isabelle_DOF-Example-Extra/technical_report/TR_my_commented_isabelle/ROOT rename to Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/ROOT diff --git a/Isabelle_DOF-Example-Extra/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy b/Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy similarity index 100% rename from Isabelle_DOF-Example-Extra/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy rename to Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy diff --git a/Isabelle_DOF-Example-Extra/technical_report/TR_my_commented_isabelle/document/figures/MyCommentedIsabelle.png b/Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/document/figures/MyCommentedIsabelle.png similarity index 100% rename from Isabelle_DOF-Example-Extra/technical_report/TR_my_commented_isabelle/document/figures/MyCommentedIsabelle.png rename to Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/document/figures/MyCommentedIsabelle.png diff --git a/Isabelle_DOF-Example-Extra/technical_report/TR_my_commented_isabelle/document/figures/document-model.pdf b/Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/document/figures/document-model.pdf similarity index 100% rename from Isabelle_DOF-Example-Extra/technical_report/TR_my_commented_isabelle/document/figures/document-model.pdf rename to Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/document/figures/document-model.pdf diff --git a/Isabelle_DOF-Example-Extra/technical_report/TR_my_commented_isabelle/document/figures/isabelle-architecture.pdf b/Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/document/figures/isabelle-architecture.pdf similarity index 100% rename from Isabelle_DOF-Example-Extra/technical_report/TR_my_commented_isabelle/document/figures/isabelle-architecture.pdf rename to Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/document/figures/isabelle-architecture.pdf diff --git a/Isabelle_DOF-Example-Extra/technical_report/TR_my_commented_isabelle/document/figures/markup-demo.png b/Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/document/figures/markup-demo.png similarity index 100% rename from Isabelle_DOF-Example-Extra/technical_report/TR_my_commented_isabelle/document/figures/markup-demo.png rename to Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/document/figures/markup-demo.png diff --git a/Isabelle_DOF-Example-Extra/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-I.pdf b/Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-I.pdf similarity index 100% rename from Isabelle_DOF-Example-Extra/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-I.pdf rename to Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-I.pdf diff --git a/Isabelle_DOF-Example-Extra/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-II.pdf b/Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-II.pdf similarity index 100% rename from Isabelle_DOF-Example-Extra/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-II.pdf rename to Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-II.pdf diff --git a/Isabelle_DOF-Example-Extra/technical_report/TR_my_commented_isabelle/document/figures/text-element.pdf b/Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/document/figures/text-element.pdf similarity index 100% rename from Isabelle_DOF-Example-Extra/technical_report/TR_my_commented_isabelle/document/figures/text-element.pdf rename to Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/document/figures/text-element.pdf diff --git a/Isabelle_DOF-Example-Extra/technical_report/TR_my_commented_isabelle/document/preamble.tex b/Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/document/preamble.tex similarity index 100% rename from Isabelle_DOF-Example-Extra/technical_report/TR_my_commented_isabelle/document/preamble.tex rename to Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/document/preamble.tex diff --git a/Isabelle_DOF-Example-Extra/technical_report/TR_my_commented_isabelle/document/prooftree.sty b/Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/document/prooftree.sty similarity index 100% rename from Isabelle_DOF-Example-Extra/technical_report/TR_my_commented_isabelle/document/prooftree.sty rename to Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/document/prooftree.sty diff --git a/Isabelle_DOF-Example-Extra/technical_report/TR_my_commented_isabelle/document/root.bib b/Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/document/root.bib similarity index 100% rename from Isabelle_DOF-Example-Extra/technical_report/TR_my_commented_isabelle/document/root.bib rename to Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/document/root.bib diff --git a/ROOTS b/ROOTS index 64ad9ea..9366b90 100644 --- a/ROOTS +++ b/ROOTS @@ -4,4 +4,4 @@ Isabelle_DOF-Ontologies Isabelle_DOF-Unit-Tests Isabelle_DOF-Example-I Isabelle_DOF-Example-II -Isabelle_DOF-Example-Extra +Isabelle_DOF-Examples-Extra