Initial commit.

.ci/Jenkinsfile

@@ -0,0 +1,26 @@
+pipeline {
+    agent any
+
+    stages {
+        stage('Build Docker') {
+            steps {
+                sh 'cp patches/thy_output.ML .ci/isabelle4isadof/'
+                sh 'docker build -t logicalhacking:isabelle4dof .ci/isabelle4isadof'
+                sh 'rm -f .ci/isabelle4isadof/thy_output.ML'
+            }
+        }
+        stage('Check Docker') {
+            when { changeset "patches/*" } 
+            steps {
+                sh 'cp patches/thy_output.ML .ci/isabelle4isadof/'
+                sh 'docker build --no-cache -t logicalhacking:isabelle4dof .ci/isabelle4isadof'
+                sh 'rm -f .ci/isabelle4isadof/thy_output.ML'
+            }
+        }
+        stage('Build Isabelle/DOF') {
+            steps {
+                sh 'docker run -v $PWD:/DOF logicalhacking:isabelle2017  sh -c "cd /DOF && ./install && isabelle build -D ."'
+            } 
+	}
+    }
+} 

.ci/isabelle4isadof/Dockerfile

@@ -0,0 +1,32 @@
+# Copyright (c) 2019 Achim D. Brucker
+#
+# All rights reserved.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#
+# * Redistributions of source code must retain the above copyright notice, this
+#
+# * Redistributions in binary form must reproduce the above copyright notice,
+#   this list of conditions and the following disclaimer in the documentation
+#   and/or other materials provided with the distribution.
+#
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+# AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+# IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+# DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+# FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+# DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+# SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+# CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+# OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+# OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# SPDX-License-Identifier: BSD-2-Clause
+
+FROM logicalhacking:isabelle2017
+
+WORKDIR /home/isabelle
+COPY thy_output.ML /home/isabelle/Isabelle/src/Pure/Thy
+RUN Isabelle/bin/isabelle build -s -b Functional-Automata
+