diff --git a/admin/jenkins/ci_build_all.scala b/admin/jenkins/ci_build_all.scala
--- a/admin/jenkins/ci_build_all.scala
+++ b/admin/jenkins/ci_build_all.scala
@@ -1,257 +1,257 @@
object profile extends isabelle.CI_Profile
{
import isabelle._
import java.io.FileReader
import scala.sys.process._
import org.apache.commons.configuration2._
override def clean = false
val afp = Path.explode("$AFP_BASE")
val afp_thys = afp + Path.explode("thys")
val afp_id = hg_id(afp)
sealed abstract class Status(val str: String)
{
def merge(that: Status): Status = (this, that) match {
case (Ok, s) => s
case (Failed, s) => Failed
case (Skipped, Failed) => Failed
case (Skipped, s) => Skipped
}
}
object Status
{
def merge(statuses: List[Status]): Status =
statuses.foldLeft(Ok: Status)(_ merge _)
def from_results(results: Build.Results, session: String): Status =
if (results.cancelled(session))
Skipped
else if (results(session).ok)
Ok
else
Failed
}
case object Ok extends Status("ok")
case object Skipped extends Status("skipped")
case object Failed extends Status("failed")
case class Mail(subject: String, recipients: List[String], text: String) {
import java.util._
import javax.mail._
import javax.mail.internet._
import javax.activation._
def send(): Unit = {
val authenticator = new Authenticator() {
override def getPasswordAuthentication() =
new PasswordAuthentication(System.getProperty("mail.smtp.user"), System.getProperty("mail.smtp.password"))
}
val session = Session.getDefaultInstance(System.getProperties(), authenticator)
val message = new MimeMessage(session)
message.setFrom(new InternetAddress("ci@isabelle.systems", "Isabelle/Jenkins"))
message.setSender(new InternetAddress("ge73ruk@mytum.de"))
message.setSubject(subject)
message.setText(text, "UTF-8")
message.setSentDate(new java.util.Date())
recipients.foreach { recipient =>
message.addRecipient(Message.RecipientType.TO, new InternetAddress(recipient))
}
try {
Transport.send(message)
}
catch {
case ex: MessagingException => println(s"Sending mail failed: ${ex.getMessage}")
}
}
}
class Metadata(ini: INIConfiguration)
{
def maintainers(entry: String): List[String] =
{
val config = ini.getSection(entry)
val raw =
if (config.containsKey("notify"))
config.getString("notify")
else
""
List(raw.split(','): _*).map(_.trim).filterNot(_.isEmpty)
}
def entry_of_session(info: Sessions.Info): Option[String] =
if (info.dir.dir.file == afp_thys.file)
Some(info.dir.base.implode)
else
None
def notify(name: String, result: Process_Result, info: Sessions.Info): Unit =
entry_of_session(info).foreach { entry =>
val mails = maintainers(entry)
val text =
s"""|The build for the session
| $name,
|belonging to the AFP entry
| $entry
|failed.
|
|You are receiving this mail because you are the maintainer of that AFP
|entry.
|
|The following information might help you with resolving the problem.
|
|Build log: ${Isabelle_System.getenv("BUILD_URL")}
|Isabelle ID: $isabelle_id
|AFP ID: $afp_id
|Timeout? ${result.timeout}
|Exit code: ${result.rc}
|
|Last 50 lines from stdout (if available):
|
|${result.out_lines.takeRight(50).mkString("\n")}
|
|Last 50 lines from stderr (if available):
|
|${result.err_lines.takeRight(50).mkString("\n")}
|""".stripMargin
val subject = s"Build of AFP entry $entry failed"
if (mails.isEmpty)
println(s"Entry $entry: WARNING no maintainers specified")
else
Mail(text = text, subject = subject, recipients = mails).send()
}
def group_by_entry(results: Build.Results): Map[Option[String], List[String]] =
results.sessions.toList.map { name =>
entry_of_session(results.info(name)) -> name
- }.groupBy(_._1).mapValues(_.map(_._2))
+ }.groupBy(_._1).view.mapValues(_.map(_._2)).toMap
def status_as_json(status: Map[Option[String], Status]): String =
{
val entries_strings = status.collect {
case (Some(entry), status) =>
s"""{"entry": "$entry", "status": "${status.str}"}"""
}
val entries_string = entries_strings.mkString("[", ",\n", "]")
s"""
{"build_data":
{"isabelle_id": "$isabelle_id",
"afp_id": "$afp_id",
"time": "$start_time",
"url": "${Isabelle_System.getenv("BUILD_URL")}",
"job": "${Isabelle_System.getenv("JOB_NAME")}"
},
"entries":
$entries_string
}
"""
}
def status_as_html(status: Map[Option[String], Status]): String =
{
val entries_strings = status.collect {
case (None, Failed) =>
s"
Distribution"
case (Some(entry), Failed) =>
s"""$entry"""
}
if (entries_strings.isEmpty)
""
else
entries_strings.mkString("Failed entries: ")
}
}
val status_file = Path.explode("$ISABELLE_HOME/status.json").file
val report_file = Path.explode("$ISABELLE_HOME/report.html").file
val deps_file = Path.explode("$ISABELLE_HOME/dependencies.json").file
def can_send_mails = System.getProperties().containsKey("mail.smtp.host")
def include = List(afp_thys)
def select = Nil
def pre_hook(args: List[String]) =
{
println(s"AFP id $afp_id")
if (status_file.exists())
status_file.delete()
if (report_file.exists())
report_file.delete()
File.write(report_file, "")
if (!can_send_mails)
println(s"Mail configuration not found.")
}
def post_hook(results: Build.Results) =
{
print_section("DEPENDENCIES")
println("Generating dependencies file ...")
val result = Isabelle_System.bash("isabelle afp_dependencies")
result.check
println("Writing dependencies file ...")
File.write(deps_file, result.out)
val metadata = {
val path = afp + Path.explode("metadata/metadata")
val ini = new INIConfiguration()
if (path.is_file) {
val reader = new FileReader(path.file)
ini.read(reader)
reader.close()
}
new Metadata(ini)
}
val status =
- metadata.group_by_entry(results).mapValues { sessions =>
+ metadata.group_by_entry(results).view.mapValues { sessions =>
Status.merge(sessions.map(Status.from_results(results, _)))
- }
+ }.toMap
print_section("REPORT")
println("Writing report file ...")
File.write(report_file, metadata.status_as_html(status))
print_section("SITEGEN")
println("Writing status file ...")
File.write(status_file, metadata.status_as_json(status))
println("Running sitegen ...")
val script = afp + Path.explode("admin/sitegen-devel")
val sitegen_result = List(script.file.toString, status_file.toString, deps_file.toString).!
if (sitegen_result > 0)
println("sitegen failed")
if (!results.ok)
{
print_section("NOTIFICATIONS")
for (name <- results.sessions)
{
val result = results(name)
if (!result.ok && !results.cancelled(name) && can_send_mails)
metadata.notify(name, result, results.info(name))
}
}
print_section("COMPLETED")
}
def selection =
Sessions.Selection(
all_sessions = true,
exclude_session_groups = List("slow"))
}
diff --git a/admin/jenkins/ci_build_testboard.scala b/admin/jenkins/ci_build_testboard.scala
--- a/admin/jenkins/ci_build_testboard.scala
+++ b/admin/jenkins/ci_build_testboard.scala
@@ -1,114 +1,114 @@
object profile extends isabelle.CI_Profile
{
import isabelle._
import java.io.FileReader
import scala.sys.process._
import org.apache.commons.configuration2._
override def clean = false
val afp = Path.explode("$AFP_BASE")
val afp_thys = afp + Path.explode("thys")
val afp_id = hg_id(afp)
sealed abstract class Status(val str: String)
{
def merge(that: Status): Status = (this, that) match {
case (Ok, s) => s
case (Failed, s) => Failed
case (Skipped, Failed) => Failed
case (Skipped, s) => Skipped
}
}
object Status
{
def merge(statuses: List[Status]): Status =
statuses.foldLeft(Ok: Status)(_ merge _)
def from_results(results: Build.Results, session: String): Status =
if (results.cancelled(session))
Skipped
else if (results(session).ok)
Ok
else
Failed
}
case object Ok extends Status("ok")
case object Skipped extends Status("skipped")
case object Failed extends Status("failed")
class Metadata(ini: INIConfiguration)
{
def entry_of_session(info: Sessions.Info): Option[String] =
if (info.dir.dir.file == afp_thys.file)
Some(info.dir.base.implode)
else
None
def group_by_entry(results: Build.Results): Map[Option[String], List[String]] =
results.sessions.toList.map { name =>
entry_of_session(results.info(name)) -> name
- }.groupBy(_._1).mapValues(_.map(_._2))
+ }.groupBy(_._1).view.mapValues(_.map(_._2)).toMap
def status_as_html(status: Map[Option[String], Status]): String =
{
val entries_strings = status.collect {
case (None, Failed) =>
s"Distribution"
case (Some(entry), Failed) =>
s"""$entry"""
}
if (entries_strings.isEmpty)
""
else
entries_strings.mkString("Failed entries: ")
}
}
val report_file = Path.explode("$ISABELLE_HOME/report.html").file
def include = List(afp_thys)
def select = Nil
def pre_hook(args: List[String]) =
{
println(s"AFP id $afp_id")
if (report_file.exists())
report_file.delete()
File.write(report_file, "")
}
def post_hook(results: Build.Results) =
{
val metadata = {
val path = afp + Path.explode("metadata/metadata")
val ini = new INIConfiguration()
if (path.is_file) {
val reader = new FileReader(path.file)
ini.read(reader)
reader.close()
}
new Metadata(ini)
}
val status =
- metadata.group_by_entry(results).mapValues { sessions =>
+ metadata.group_by_entry(results).view.mapValues { sessions =>
Status.merge(sessions.map(Status.from_results(results, _)))
- }
+ }.toMap
print_section("REPORT")
println("Writing report file ...")
File.write(report_file, metadata.status_as_html(status))
print_section("COMPLETED")
}
def selection =
Sessions.Selection(
all_sessions = true,
exclude_session_groups = List("slow"))
}
diff --git a/thys/FOL_Seq_Calc1/Common.thy b/thys/FOL_Seq_Calc1/Common.thy
--- a/thys/FOL_Seq_Calc1/Common.thy
+++ b/thys/FOL_Seq_Calc1/Common.thy
@@ -1,14 +1,18 @@
(*
- Author: Asta Halkjær From, DTU Compute, 2019
+ Author: Asta Halkjær From, DTU Compute, 2019-2021
Contributors: Alexander Birch Jensen, Anders Schlichtkrull & Jørgen Villadsen
- See also the Natural Deduction Assistant: https://nadea.compute.dtu.dk/
+
+ See also the Natural Deduction Assistant (NaDeA) and the Sequent Calculus Verifier (SeCaV):
+
+ https://nadea.compute.dtu.dk/
+ https://secav.compute.dtu.dk/
*)
section \Common Notation\
theory Common imports "FOL-Fitting.FOL_Fitting" begin
notation FF (\\\)
notation TT (\\\)
end
diff --git a/thys/FOL_Seq_Calc1/Sequent.thy b/thys/FOL_Seq_Calc1/Sequent.thy
--- a/thys/FOL_Seq_Calc1/Sequent.thy
+++ b/thys/FOL_Seq_Calc1/Sequent.thy
@@ -1,205 +1,209 @@
(*
- Author: Asta Halkjær From, DTU Compute, 2019
+ Author: Asta Halkjær From, DTU Compute, 2019-2021
Contributors: Alexander Birch Jensen, Anders Schlichtkrull & Jørgen Villadsen
- See also the Natural Deduction Assistant: https://nadea.compute.dtu.dk/
+
+ See also the Natural Deduction Assistant (NaDeA) and the Sequent Calculus Verifier (SeCaV):
+
+ https://nadea.compute.dtu.dk/
+ https://secav.compute.dtu.dk/
*)
section \Sequent Calculus\
theory Sequent imports Tableau begin
inductive SC :: \('a, 'b) form list \ bool\ (\\ _\ 0) where
Basic: \\ Pred i l # Neg (Pred i l) # G\
| BasicNegFF: \\ Neg \ # G\
| BasicTT: \\ \ # G\
| AlphaNegNeg: \\ A # G \ \ Neg (Neg A) # G\
| AlphaNegAnd: \\ Neg A # Neg B # G \ \ Neg (And A B) # G\
| AlphaOr: \\ A # B # G \ \ Or A B # G\
| AlphaImpl: \\ Neg A # B # G \ \ Impl A B # G\
| BetaAnd: \\ A # G \ \ B # G \ \ And A B # G\
| BetaNegOr: \\ Neg A # G \ \ Neg B # G \ \ Neg (Or A B) # G\
| BetaNegImpl: \\ A # G \ \ Neg B # G \ \ Neg (Impl A B) # G\
| GammaExists: \\ subst A t 0 # G \ \ Exists A # G\
| GammaNegForall: \\ Neg (subst A t 0) # G \ \ Neg (Forall A) # G\
| DeltaForall: \\ subst A (App n []) 0 # G \ news n (A # G) \ \ Forall A # G\
| DeltaNegExists: \\ Neg (subst A (App n []) 0) # G \ news n (A # G) \ \ Neg (Exists A) # G\
| Order: \\ G \ set G = set G' \ \ G'\
lemma Shift: \\ rotate1 G \ \ G\
by (simp add: Order)
lemma Swap: \\ B # A # G \ \ A # B # G\
by (simp add: Order insert_commute)
lemma \\ [Neg (Pred ''A'' []), Pred ''A'' []]\
by (rule Shift, simp) (rule Basic)
lemma \\ [And (Pred ''A'' []) (Pred ''B'' []), Neg (And (Pred ''B'' []) (Pred ''A'' []))]\
apply (rule BetaAnd)
apply (rule Swap)
apply (rule AlphaNegAnd)
apply (rule Shift, simp, rule Swap)
apply (rule Basic)
apply (rule Swap)
apply (rule AlphaNegAnd)
apply (rule Shift, rule Shift, simp)
apply (rule Basic)
done
subsection \Soundness\
lemma SC_soundness: \\ G \ \p \ set G. eval e f g p\
proof (induct G arbitrary: f rule: SC.induct)
case (DeltaForall A n G)
then consider
\\x. eval e (f(n := \w. x)) g (subst A (App n []) 0)\ |
\\x. \p \ set G. eval e (f(n := \w. x)) g p\
by fastforce
then show ?case
proof cases
case 1
then have \\x. eval (shift e 0 x) (f(n := \w. x)) g A\
by simp
then have \\x. eval (shift e 0 x) f g A\
using \news n (A # G)\ by simp
then show ?thesis
by simp
next
case 2
then have \\p \ set G. eval e f g p\
using \news n (A # G)\ using Ball_set insert_iff list.set(2) upd_lemma by metis
then show ?thesis
by simp
qed
next
case (DeltaNegExists A n G)
then consider
\\x. eval e (f(n := \w. x)) g (Neg (subst A (App n []) 0))\ |
\\x. \p \ set G. eval e (f(n := \w. x)) g p\
by fastforce
then show ?case
proof cases
case 1
then have \\x. eval (shift e 0 x) (f(n := \w. x)) g (Neg A)\
by simp
then have \\x. eval (shift e 0 x) f g (Neg A)\
using \news n (A # G)\ by simp
then show ?thesis
by simp
next
case 2
then have \\p \ set G. eval e f g p\
using \news n (A # G)\ using Ball_set insert_iff list.set(2) upd_lemma by metis
then show ?thesis
by simp
qed
qed auto
subsection \Tableau Calculus Equivalence\
fun compl :: \('a, 'b) form \ ('a, 'b) form\ where
\compl (Neg p) = p\
| \compl p = Neg p\
lemma compl: \compl p = Neg p \ (\q. compl p = q \ p = Neg q)\
by (cases p rule: compl.cases) simp_all
lemma new_compl: \new n p \ new n (compl p)\
by (cases p rule: compl.cases) simp_all
lemma news_compl: \news n G \ news n (map compl G)\
using new_compl by (induct G) fastforce+
theorem TC_SC: \\ G \ \ map compl G\
proof (induct G rule: TC.induct)
case (Basic i l G)
then show ?case
using SC.Basic Swap by fastforce
next
case (AlphaNegNeg A G)
then show ?case
using SC.AlphaNegNeg compl by (metis compl.simps(1) list.simps(9))
next
case (AlphaAnd A B G)
then have *: \\ compl A # compl B # map compl G\
by simp
then have \\ Neg A # Neg B # map compl G\
using compl AlphaNegNeg Swap by metis
then show ?case
using AlphaNegAnd by simp
next
case (AlphaNegImpl A B G)
then have \\ compl A # B # map compl G\
by simp
then have \\ Neg A # B # map compl G\
using compl AlphaNegNeg by metis
then show ?case
using AlphaImpl by simp
next
case (BetaOr A G B)
then have \\ compl A # map compl G\ \\ compl B # map compl G\
by simp_all
then have \\ Neg A # map compl G\ \\ Neg B # map compl G\
using compl AlphaNegNeg by metis+
then show ?case
using BetaNegOr by simp
next
case (BetaImpl A G B)
then have \\ A # map compl G\ \\ compl B # map compl G\
by simp_all
then have \\ A # map compl G\ \\ Neg B # map compl G\
by - (assumption, metis compl AlphaNegNeg)
then have \\ Neg (Impl A B) # map compl G\
using BetaNegImpl by blast
then have \\ compl (Impl A B) # map compl G\
using \\ A # map compl G\ compl by simp
then show ?case
by simp
next
case (GammaForall A t G)
then have \\ compl (subst A t 0) # map compl G\
by simp
then have \\ Neg (subst A t 0) # map compl G\
using compl AlphaNegNeg by metis
then show ?case
using GammaNegForall by simp
next
case (DeltaExists A n G)
then have \\ compl (subst A (App n []) 0) # map compl G\
by simp
then have \\ Neg (subst A (App n []) 0) # map compl G\
using compl AlphaNegNeg by metis
moreover have \news n (A # map compl G)\