--- a/NEWS Mon Jan 03 13:28:31 2022 +0100
+++ b/NEWS Mon Jan 03 13:29:05 2022 +0100
@@ -45,6 +45,15 @@
in TH0 and TH1.
+*** System ***
+
+* Command-line tool "isabelle scala_project" supports Gradle as
+alternative to Maven: either option -G or -M needs to be specified
+explicitly. This increases the chances that the Java/Scala IDE project
+works properly.
+
+
+
New in Isabelle2021-1 (December 2021)
-------------------------------------
--- a/src/Doc/System/Scala.thy Mon Jan 03 13:28:31 2022 +0100
+++ b/src/Doc/System/Scala.thy Mon Jan 03 13:29:05 2022 +0100
@@ -266,7 +266,7 @@
text \<open>
The @{tool_def scala_project} tool creates a project configuration for all
- Isabelle/Scala/Java modules specified in components via
+ Isabelle/Java/Scala modules specified in components via
\<^path>\<open>etc/build.props\<close>, together with additional source files given on
the command-line:
@@ -275,22 +275,32 @@
Options are:
-D DIR project directory (default: "$ISABELLE_HOME_USER/scala_project")
+ -G use Gradle as build tool
-L make symlinks to original source files
+ -M use Maven as build tool
-f force update of existing directory
- Setup Maven project for Isabelle/Scala/jEdit --- to support common IDEs
- such as IntelliJ IDEA.\<close>}
+ Setup project for Isabelle/Scala/jEdit --- to support common IDEs such
+ as IntelliJ IDEA. Either option -G or -M is mandatory to specify the
+ build tool.\<close>}
- The generated configuration is for Maven\<^footnote>\<open>\<^url>\<open>https://maven.apache.org\<close>\<close>, but
- the main purpose is to import it into common IDEs, such as IntelliJ
- IDEA\<^footnote>\<open>\<^url>\<open>https://www.jetbrains.com/idea\<close>\<close>. This allows to explore the
- sources with static analysis and other hints in real-time.
+ The generated configuration is for Gradle\<^footnote>\<open>\<^url>\<open>https://gradle.org\<close>\<close> or
+ Maven\<^footnote>\<open>\<^url>\<open>https://maven.apache.org\<close>\<close>, but the main purpose is to import it
+ into common IDEs like IntelliJ IDEA\<^footnote>\<open>\<^url>\<open>https://www.jetbrains.com/idea\<close>\<close>.
+ This allows to explore the sources with static analysis and other hints in
+ real-time.
The generated files refer to physical file-system locations, using the path
notation of the underlying OS platform. Thus the project needs to be
recreated whenever the Isabelle installation is changed or moved.
\<^medskip>
+ Option \<^verbatim>\<open>-G\<close> selects Gradle and \<^verbatim>\<open>-M\<close> selects Maven as Java/Scala build
+ tool: either one needs to be specified explicitly. These tools have a
+ tendency to break down unexpectedly, so supporting both increases the
+ chances that the generated IDE project works properly.
+
+ \<^medskip>
Option \<^verbatim>\<open>-L\<close> produces \<^emph>\<open>symlinks\<close> to the original files: this allows to
develop Isabelle/Scala/jEdit modules within an external IDE. The default is
to \<^emph>\<open>copy\<close> source files, so editing them within the IDE has no permanent
--- a/src/HOL/GCD.thy Mon Jan 03 13:28:31 2022 +0100
+++ b/src/HOL/GCD.thy Mon Jan 03 13:29:05 2022 +0100
@@ -1637,6 +1637,26 @@
end
+text \<open>And some consequences: cancellation modulo @{term m}\<close>
+lemma mult_mod_cancel_right:
+ fixes m :: "'a::{euclidean_ring_cancel,semiring_gcd}"
+ assumes eq: "(a * n) mod m = (b * n) mod m" and "coprime m n"
+ shows "a mod m = b mod m"
+proof -
+ have "m dvd (a*n - b*n)"
+ using eq mod_eq_dvd_iff by blast
+ then have "m dvd a-b"
+ by (metis \<open>coprime m n\<close> coprime_dvd_mult_left_iff left_diff_distrib')
+ then show ?thesis
+ using mod_eq_dvd_iff by blast
+qed
+
+lemma mult_mod_cancel_left:
+ fixes m :: "'a::{euclidean_ring_cancel,semiring_gcd}"
+ assumes "(n * a) mod m = (n * b) mod m" and "coprime m n"
+ shows "a mod m = b mod m"
+ by (metis assms mult.commute mult_mod_cancel_right)
+
subsection \<open>GCD and LCM for multiplicative normalisation functions\<close>
--- a/src/HOL/Library/Nat_Bijection.thy Mon Jan 03 13:28:31 2022 +0100
+++ b/src/HOL/Library/Nat_Bijection.thy Mon Jan 03 13:29:05 2022 +0100
@@ -87,10 +87,10 @@
lemma bij_prod_decode: "bij prod_decode"
by (rule bijI [OF inj_prod_decode surj_prod_decode])
-lemma prod_encode_eq: "prod_encode x = prod_encode y \<longleftrightarrow> x = y"
+lemma prod_encode_eq [simp]: "prod_encode x = prod_encode y \<longleftrightarrow> x = y"
by (rule inj_prod_encode [THEN inj_eq])
-lemma prod_decode_eq: "prod_decode x = prod_decode y \<longleftrightarrow> x = y"
+lemma prod_decode_eq [simp]: "prod_decode x = prod_decode y \<longleftrightarrow> x = y"
by (rule inj_prod_decode [THEN inj_eq])
--- a/src/HOL/List.thy Mon Jan 03 13:28:31 2022 +0100
+++ b/src/HOL/List.thy Mon Jan 03 13:29:05 2022 +0100
@@ -1244,6 +1244,9 @@
lemma rev_eq_Cons_iff[iff]: "(rev xs = y#ys) = (xs = rev ys @ [y])"
by(rule rev_cases[of xs]) auto
+lemma length_Suc_conv_rev: "(length xs = Suc n) = (\<exists>y ys. xs = ys @ [y] \<and> length ys = n)"
+by (induct xs rule: rev_induct) auto
+
subsubsection \<open>\<^const>\<open>set\<close>\<close>
--- a/src/HOL/Set_Interval.thy Mon Jan 03 13:28:31 2022 +0100
+++ b/src/HOL/Set_Interval.thy Mon Jan 03 13:29:05 2022 +0100
@@ -22,6 +22,9 @@
lemma card_2_iff': "card S = 2 \<longleftrightarrow> (\<exists>x\<in>S. \<exists>y\<in>S. x \<noteq> y \<and> (\<forall>z\<in>S. z = x \<or> z = y))"
by (auto simp: card_Suc_eq numeral_eq_Suc)
+lemma card_3_iff: "card S = 3 \<longleftrightarrow> (\<exists>x y z. S = {x,y,z} \<and> x \<noteq> y \<and> y \<noteq> z \<and> x \<noteq> z)"
+ by (fastforce simp: card_Suc_eq numeral_eq_Suc)
+
context ord
begin
--- a/src/Pure/General/json_api.scala Mon Jan 03 13:28:31 2022 +0100
+++ b/src/Pure/General/json_api.scala Mon Jan 03 13:29:05 2022 +0100
@@ -6,6 +6,8 @@
package isabelle
+import java.net.URL
+
object JSON_API
{
@@ -14,11 +16,25 @@
def api_error(msg: String): Nothing = error("JSON API error: " + msg)
def api_errors(msgs: List[String]): Nothing = error(("JSON API errors:" :: msgs).mkString("\n "))
+ class Service(val url: URL)
+ {
+ override def toString: String = url.toString
+
+ def get(route: String): HTTP.Content =
+ HTTP.Client.get(if (route.isEmpty) url else new URL(url, route))
+
+ def get_root(route: String = ""): Root =
+ Root(get(if (route.isEmpty) "" else "/" + route).json)
+ }
+
sealed case class Root(json: JSON.T)
{
def get_links: Option[Links] = JSON.value(json, "links").map(Links)
+ def get_next: Option[Service] = get_links.flatMap(_.get_next)
+
def get_included: List[Resource] = JSON.list(json, "included", Resource.some).getOrElse(Nil)
def get_data: Option[Data] = JSON.value(json, "data").map(Data(_, get_included))
+
def get_errors: Option[List[JSON.T]] = JSON.list(json, "errors", Some(_))
def ok: Boolean = get_errors.isEmpty
@@ -29,14 +45,38 @@
case Some(errs) => api_errors(errs.map(JSON.Format.apply))
}
def check_data: Data = check.get_data getOrElse api_error("missing data")
+ def check_resource: Resource = check_data.resource
+ def check_resources: List[Resource] = check_data.resources
+
+ def iterator: Iterator[Root] =
+ {
+ val init = Some(this)
+ new Iterator[Root] {
+ private var state: Option[Root] = init
+ def hasNext: Boolean = state.nonEmpty
+ def next(): Root =
+ state match {
+ case None => Iterator.empty.next()
+ case Some(res) =>
+ state = res.get_next.map(_.get_root())
+ res
+ }
+ }
+ }
+ def iterator_data: Iterator[Data] = iterator.map(_.check_data)
+ def iterator_resource: Iterator[Resource] = iterator.map(_.check_resource)
+ def iterator_resources: Iterator[Resource] = iterator.flatMap(_.check_resources)
override def toString: String = "Root(" + (if (ok) "ok" else "errors") + ")"
}
sealed case class Links(json: JSON.T)
{
- def get_next: Option[Root] =
- for (next <- JSON.value(json, "next") if next != null) yield Root(next)
+ def get_next: Option[Service] =
+ for {
+ JSON.Value.String(next) <- JSON.value(json, "next")
+ if Url.is_wellformed(next)
+ } yield new Service(Url(next))
override def toString: String =
if (get_next.isEmpty) "Links()" else "Links(next)"
--- a/src/Pure/Isar/outer_syntax.ML Mon Jan 03 13:28:31 2022 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Mon Jan 03 13:29:05 2022 +0100
@@ -162,7 +162,9 @@
(Restricted_Parser (fn restricted =>
Parse.opt_target -- parse >> (fn (target, f) => trans restricted target f)));
-val local_theory' = local_theory_command Toplevel.local_theory';
+val local_theory' =
+ local_theory_command
+ (fn a => fn b => fn c => Toplevel.local_theory' a b c Toplevel.no_presentation);
val local_theory = local_theory_command Toplevel.local_theory;
val local_theory_to_proof' = local_theory_command Toplevel.local_theory_to_proof';
val local_theory_to_proof = local_theory_command Toplevel.local_theory_to_proof;
--- a/src/Pure/Isar/toplevel.ML Mon Jan 03 13:28:31 2022 +0100
+++ b/src/Pure/Isar/toplevel.ML Mon Jan 03 13:29:05 2022 +0100
@@ -32,6 +32,8 @@
val string_of_state: state -> string
val pretty_abstract: state -> Pretty.T
type presentation = state -> Latex.text option
+ val presentation: (state -> Latex.text) -> presentation
+ val no_presentation: presentation
type transition
val empty: transition
val name_of: transition -> string
@@ -55,14 +57,14 @@
val ignored: Position.T -> transition
val malformed: Position.T -> string -> transition
val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
- val theory': (bool -> theory -> theory) -> transition -> transition
+ val theory': (bool -> theory -> theory) -> presentation -> transition -> transition
val theory: (theory -> theory) -> transition -> transition
val begin_main_target: bool -> (theory -> local_theory) -> transition -> transition
val end_main_target: transition -> transition
val begin_nested_target: (Context.generic -> local_theory) -> transition -> transition
val end_nested_target: transition -> transition
val local_theory': (bool * Position.T) option -> (xstring * Position.T) option ->
- (bool -> local_theory -> local_theory) -> transition -> transition
+ (bool -> local_theory -> local_theory) -> presentation -> transition -> transition
val local_theory: (bool * Position.T) option -> (xstring * Position.T) option ->
(local_theory -> local_theory) -> transition -> transition
val present_local_theory: (xstring * Position.T) option -> (state -> Latex.text) ->
@@ -267,8 +269,8 @@
(* presentation *)
type presentation = state -> Latex.text option;
+fun presentation g : presentation = SOME o g;
val no_presentation: presentation = K NONE;
-fun presentation g : presentation = SOME o g;
(* primitive transitions *)
@@ -452,7 +454,7 @@
(fn Theory gthy => node_presentation (Theory (f gthy))
| _ => raise UNDEF));
-fun theory' f = transaction (fn int =>
+fun theory' f = present_transaction (fn int =>
(fn Theory (Context.Theory thy) =>
let val thy' = thy
|> Sign.new_group
@@ -461,7 +463,7 @@
in node_presentation (Theory (Context.Theory thy')) end
| _ => raise UNDEF));
-fun theory f = theory' (K f);
+fun theory f = theory' (K f) no_presentation;
fun begin_main_target begin f = transaction (fn _ =>
(fn Theory (Context.Theory thy) =>
@@ -510,10 +512,10 @@
|> f int
|> Local_Theory.reset_group;
in (Theory (finish lthy'), lthy') end
- | _ => raise UNDEF))
- no_presentation;
+ | _ => raise UNDEF));
-fun local_theory restricted target f = local_theory' restricted target (K f);
+fun local_theory restricted target f =
+ local_theory' restricted target (K f) no_presentation;
fun present_local_theory target g = present_transaction (fn _ =>
(fn Theory gthy =>
--- a/src/Pure/Tools/flarum.scala Mon Jan 03 13:28:31 2022 +0100
+++ b/src/Pure/Tools/flarum.scala Mon Jan 03 13:29:05 2022 +0100
@@ -13,20 +13,18 @@
object Flarum
{
// see RFC3339 in https://www.php.net/manual/en/class.datetimeinterface.php
- val Date_Format = Date.Format("uuuu-MM-dd'T'HH:mm:ssxxx")
+ val Date_Format: Date.Format = Date.Format("uuuu-MM-dd'T'HH:mm:ssxxx")
def server(url: URL): Server = new Server(url)
- class Server private[Flarum](url: URL)
+ class Server private[Flarum](url: URL) extends JSON_API.Service(url)
{
- override def toString: String = url.toString
+ def get_api(route: String): JSON_API.Root =
+ get_root("api" + (if (route.isEmpty) "" else "/" + route))
- def get(route: String): HTTP.Content =
- HTTP.Client.get(if (route.isEmpty) url else new URL(url, route))
-
- def get_api(route: String = ""): JSON_API.Root =
- JSON_API.Root(get("api" + (if (route.isEmpty) "" else "/" + route)).json)
-
- val api: JSON_API.Root = get_api()
+ val root: JSON_API.Root = get_api("")
+ def users: JSON_API.Root = get_api("users")
+ def groups: JSON_API.Root = get_api("groups")
+ def discussions: JSON_API.Root = get_api("discussions")
}
}
--- a/src/Pure/Tools/scala_project.scala Mon Jan 03 13:28:31 2022 +0100
+++ b/src/Pure/Tools/scala_project.scala Mon Jan 03 13:29:05 2022 +0100
@@ -1,8 +1,8 @@
/* Title: Pure/Tools/scala_project.scala
Author: Makarius
-Manage Isabelle/Scala/Java project sources, with output to Maven for
-IntelliJ IDEA.
+Manage Isabelle/Scala/Java project sources, with output to Gradle or
+Maven for IntelliJ IDEA.
*/
package isabelle
@@ -10,17 +10,95 @@
object Scala_Project
{
- /* Maven project */
+ /** build tools **/
def java_version: String = "15"
def scala_version: String = scala.util.Properties.versionNumberString
- def maven_project(jars: List[Path]): String =
+ abstract class Build_Tool
+ {
+ def project_root: Path
+ def init_project(dir: Path, jars: List[Path]): Unit
+
+ val java_src_dir: Path = Path.explode("src/main/java")
+ val scala_src_dir: Path = Path.explode("src/main/scala")
+
+ def detect_project(dir: Path): Boolean =
+ (dir + project_root).is_file &&
+ (dir + scala_src_dir).is_dir
+
+ def package_dir(source_file: Path): Path =
+ {
+ val is_java = source_file.is_java
+ val dir =
+ package_name(source_file) match {
+ case Some(name) =>
+ if (is_java) Path.explode(space_explode('.', name).mkString("/"))
+ else Path.basic(name)
+ case None => error("Failed to guess package from " + source_file)
+ }
+ (if (is_java) java_src_dir else scala_src_dir) + dir
+ }
+ }
+
+ def build_tools: List[Build_Tool] = List(Gradle, Maven)
+
+
+ /* Gradle */
+
+ object Gradle extends Build_Tool
{
- def dependency(jar: Path): String =
+ override def toString: String = "Gradle"
+
+ val project_settings: Path = Path.explode("settings.gradle")
+ override val project_root: Path = Path.explode("build.gradle")
+
+ private def groovy_string(s: String): String =
+ {
+ s.map(c =>
+ c match {
+ case '\t' | '\b' | '\n' | '\r' | '\f' | '\\' | '\'' | '"' => "\\" + c
+ case _ => c.toString
+ }).mkString("'", "", "'")
+ }
+
+ override def init_project(dir: Path, jars: List[Path]): Unit =
{
- val name = jar.expand.drop_ext.base.implode
- val system_path = File.platform_path(jar.absolute)
+ File.write(dir + project_settings, "rootProject.name = 'Isabelle'\n")
+ File.write(dir + project_root,
+"""plugins {
+ id 'scala'
+}
+
+repositories {
+ mavenCentral()
+}
+
+dependencies {
+ implementation 'org.scala-lang:scala-library:""" + scala_version + """'
+ compileOnly files(
+ """ + jars.map(jar => groovy_string(File.platform_path(jar))).mkString("", ",\n ", ")") +
+"""
+}
+""")
+ }
+ }
+
+
+ /* Maven */
+
+ object Maven extends Build_Tool
+ {
+ override def toString: String = "Maven"
+
+ override val project_root: Path = Path.explode("pom.xml")
+
+ override def init_project(dir: Path, jars: List[Path]): Unit =
+ {
+ def dependency(jar: Path): String =
+ {
+ val name = jar.expand.drop_ext.base.implode
+ val system_path = File.platform_path(jar.absolute)
""" <dependency>
<groupId>classpath</groupId>
<artifactId>""" + XML.text(name) + """</artifactId>
@@ -28,9 +106,9 @@
<scope>system</scope>
<systemPath>""" + XML.text(system_path) + """</systemPath>
</dependency>"""
- }
+ }
- """<?xml version="1.0" encoding="UTF-8"?>
+ val project = """<?xml version="1.0" encoding="UTF-8"?>
<project xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
<modelVersion>4.0.0</modelVersion>
@@ -60,6 +138,9 @@
<dependencies>""" + jars.map(dependency).mkString("\n", "\n", "\n") + """</dependencies>
</project>"""
+
+ File.write(dir + project_root, project)
+ }
}
@@ -148,17 +229,8 @@
lines.collectFirst({ case Package(name) => name })
}
- def the_package_dir(source_file: Path): Path =
- {
- package_name(source_file) match {
- case Some(name) =>
- if (source_file.is_java) Path.explode(space_explode('.', name).mkString("/"))
- else Path.basic(name)
- case None => error("Failed to guess package from " + source_file)
- }
- }
-
def scala_project(
+ build_tool: Build_Tool,
project_dir: Path = default_project_dir,
more_sources: List[Path] = Nil,
symlinks: Boolean = false,
@@ -166,10 +238,7 @@
progress: Progress = new Progress): Unit =
{
if (project_dir.file.exists) {
- val detect =
- project_dir.is_dir &&
- (project_dir + Path.explode("pom.xml")).is_file &&
- (project_dir + Path.explode("src/main/scala")).is_dir
+ val detect = project_dir.is_dir && build_tools.exists(_.detect_project(project_dir))
if (force && detect) {
progress.echo("Purging existing project directory: " + project_dir.absolute)
@@ -178,19 +247,19 @@
else error("Project directory already exists: " + project_dir.absolute)
}
- progress.echo("Creating project directory: " + project_dir.absolute)
+ progress.echo("Creating " + build_tool + " project directory: " + project_dir.absolute)
Isabelle_System.make_directory(project_dir)
- val java_src_dir = Isabelle_System.make_directory(Path.explode("src/main/java"))
- val scala_src_dir = Isabelle_System.make_directory(Path.explode("src/main/scala"))
+ val java_src_dir = Isabelle_System.make_directory(project_dir + build_tool.java_src_dir)
+ val scala_src_dir = Isabelle_System.make_directory(project_dir + build_tool.scala_src_dir)
val (jars, sources) = isabelle_files
isabelle_scala_files
- File.write(project_dir + Path.explode("pom.xml"), maven_project(jars))
+ build_tool.init_project(project_dir, jars)
for (source <- sources ::: more_sources) {
- val dir = (if (source.is_java) java_src_dir else scala_src_dir) + the_package_dir(source)
+ val dir = build_tool.package_dir(source)
val target_dir = project_dir + dir
if (!target_dir.is_dir) {
progress.echo(" Creating package directory: " + dir)
@@ -205,9 +274,10 @@
/* Isabelle tool wrapper */
val isabelle_tool =
- Isabelle_Tool("scala_project", "setup Maven project for Isabelle/Scala/jEdit",
+ Isabelle_Tool("scala_project", "setup IDE project for Isabelle/Java/Scala sources",
Scala_Project.here, args =>
{
+ var build_tool: Option[Build_Tool] = None
var project_dir = default_project_dir
var symlinks = false
var force = false
@@ -217,14 +287,19 @@
Options are:
-D DIR project directory (default: """ + default_project_dir + """)
+ -G use Gradle as build tool
-L make symlinks to original source files
+ -M use Maven as build tool
-f force update of existing directory
- Setup Maven project for Isabelle/Scala/jEdit --- to support common IDEs
- such as IntelliJ IDEA.
+ Setup project for Isabelle/Scala/jEdit --- to support common IDEs such
+ as IntelliJ IDEA. Either option -G or -M is mandatory to specify the
+ build tool.
""",
"D:" -> (arg => project_dir = Path.explode(arg)),
+ "G" -> (_ => build_tool = Some(Gradle)),
"L" -> (_ => symlinks = true),
+ "M" -> (_ => build_tool = Some(Maven)),
"f" -> (_ => force = true))
val more_args = getopts(args)
@@ -232,7 +307,11 @@
val more_sources = more_args.map(Path.explode)
val progress = new Console_Progress
- scala_project(project_dir = project_dir, more_sources = more_sources,
+ if (build_tool.isEmpty) {
+ error("Unspecified build tool: need to provide option -G or -M")
+ }
+
+ scala_project(build_tool.get, project_dir = project_dir, more_sources = more_sources,
symlinks = symlinks, force = force, progress = progress)
})
}