From 6ec427e716f4b4b1fb356947736f5a5f9bfd9340 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Wed, 8 Apr 2020 10:51:27 +0100 Subject: [PATCH 1/7] Cleanup. --- src/patches/thy_info.ML | 495 ----------------------------------- src/patches/thy_info.orig.ML | 484 ---------------------------------- 2 files changed, 979 deletions(-) delete mode 100644 src/patches/thy_info.ML delete mode 100644 src/patches/thy_info.orig.ML diff --git a/src/patches/thy_info.ML b/src/patches/thy_info.ML deleted file mode 100644 index 5ac4e3f9..00000000 --- a/src/patches/thy_info.ML +++ /dev/null @@ -1,495 +0,0 @@ -(* Title: Pure/Thy/thy_info.ML - Author: Markus Wenzel, TU Muenchen - -Global theory info database, with auto-loading according to theory and -file dependencies. -*) - -signature THY_INFO = -sig - type presentation_context = - {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T, - segments: Thy_Output.segment list} - val apply_presentation: presentation_context -> theory -> unit - val add_presentation: (presentation_context -> theory -> unit) -> theory -> theory - val get_names: unit -> string list - val lookup_theory: string -> theory option - val get_theory: string -> theory - val master_directory: string -> Path.T - val remove_thy: string -> unit - type context = - {options: Options.T, - symbols: HTML.symbols, - bibtex_entries: string list, - last_timing: Toplevel.transition -> Time.time} - val use_theories: context -> string -> Path.T -> (string * Position.T) list -> unit - val use_thy: string -> unit - val script_thy: Position.T -> string -> theory -> theory - val register_thy: theory -> unit - val finish: unit -> unit -end; - -structure Thy_Info: THY_INFO = -struct - -(** presentation of consolidated theory **) - -type presentation_context = - {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T, - segments: Thy_Output.segment list}; - -structure Presentation = Theory_Data -( - type T = ((presentation_context -> theory -> unit) * stamp) list; - val empty = []; - val extend = I; - fun merge data : T = Library.merge (eq_snd op =) data; -); - -fun apply_presentation (context: presentation_context) thy = - ignore (Presentation.get thy |> Par_List.map (fn (f, _) => f context thy)); - -fun add_presentation f = Presentation.map (cons (f, stamp ())); - -val _ = - Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy => - if exists (Toplevel.is_skipped_proof o #state) segments then () - else - let - val body = Thy_Output.present_thy options thy segments; - val option = Present.document_option options; - in - if #disabled option then () - else - let - val latex = Latex.isabelle_body (Context.theory_name thy) body; - val output = [Latex.output_text latex, Latex.output_positions file_pos latex]; - val _ = - if Options.bool options "export_document" - then Export.export thy "document.tex" output else (); - val _ = if #enabled option then Present.theory_output thy output else (); - in () end - end)); - - - -(** thy database **) - -(* messages *) - -val show_path = space_implode " via " o map quote; - -fun cycle_msg names = "Cyclic dependency of " ^ show_path names; - - -(* derived graph operations *) - -fun add_deps name parents G = String_Graph.add_deps_acyclic (name, parents) G - handle String_Graph.CYCLES namess => error (cat_lines (map cycle_msg namess)); - -fun new_entry name parents entry = - String_Graph.new_node (name, entry) #> add_deps name parents; - - -(* global thys *) - -type deps = - {master: (Path.T * SHA1.digest), (*master dependencies for thy file*) - imports: (string * Position.T) list}; (*source specification of imports (partially qualified)*) - -fun make_deps master imports : deps = {master = master, imports = imports}; - -fun master_dir_deps (d: deps option) = - the_default Path.current (Option.map (Path.dir o #1 o #master) d); - -local - val global_thys = - Synchronized.var "Thy_Info.thys" - (String_Graph.empty: (deps option * theory option) String_Graph.T); -in - fun get_thys () = Synchronized.value global_thys; - fun change_thys f = Synchronized.change global_thys f; -end; - -fun get_names () = String_Graph.topological_order (get_thys ()); - - -(* access thy *) - -fun lookup thys name = try (String_Graph.get_node thys) name; -fun lookup_thy name = lookup (get_thys ()) name; - -fun get thys name = - (case lookup thys name of - SOME thy => thy - | NONE => error ("Theory loader: nothing known about theory " ^ quote name)); - -fun get_thy name = get (get_thys ()) name; - - -(* access deps *) - -val lookup_deps = Option.map #1 o lookup_thy; - -val master_directory = master_dir_deps o #1 o get_thy; - - -(* access theory *) - -fun lookup_theory name = - (case lookup_thy name of - SOME (_, SOME theory) => SOME theory - | _ => NONE); - -fun get_theory name = - (case lookup_theory name of - SOME theory => theory - | _ => error ("Theory loader: undefined entry for theory " ^ quote name)); - -val get_imports = Resources.imports_of o get_theory; - - - -(** thy operations **) - -(* remove *) - -fun remove name thys = - (case lookup thys name of - NONE => thys - | SOME (NONE, _) => error ("Cannot update finished theory " ^ quote name) - | SOME _ => - let - val succs = String_Graph.all_succs thys [name]; - val _ = writeln ("Theory loader: removing " ^ commas_quote succs); - in fold String_Graph.del_node succs thys end); - -val remove_thy = change_thys o remove; - - -(* update *) - -fun update deps theory thys = - let - val name = Context.theory_long_name theory; - val parents = map Context.theory_long_name (Theory.parents_of theory); - - val thys' = remove name thys; - val _ = map (get thys') parents; - in new_entry name parents (SOME deps, SOME theory) thys' end; - -fun update_thy deps theory = change_thys (update deps theory); - - -(* context *) - -type context = - {options: Options.T, - symbols: HTML.symbols, - bibtex_entries: string list, - last_timing: Toplevel.transition -> Time.time}; - -fun default_context (): context = - {options = Options.default (), - symbols = HTML.no_symbols, - bibtex_entries = [], - last_timing = K Time.zeroTime}; - - -(* scheduling loader tasks *) - -datatype result = - Result of {theory: theory, exec_id: Document_ID.exec, - present: unit -> unit, commit: unit -> unit, weight: int}; - -fun theory_result theory = - Result {theory = theory, exec_id = Document_ID.none, present = I, commit = I, weight = 0}; - -fun result_theory (Result {theory, ...}) = theory; -fun result_present (Result {present, ...}) = present; -fun result_commit (Result {commit, ...}) = commit; -fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i); - -fun join_theory (Result {theory, exec_id, ...}) = - let - val _ = Execution.join [exec_id]; - val res = Exn.capture Thm.consolidate_theory theory; - val exns = maps Task_Queue.group_status (Execution.peek exec_id); - in res :: map Exn.Exn exns end; - -datatype task = - Task of string list * (theory list -> result) | - Finished of theory; - -fun task_finished (Task _) = false - | task_finished (Finished _) = true; - -fun task_parents deps (parents: string list) = map (the o AList.lookup (op =) deps) parents; - -val schedule_seq = - String_Graph.schedule (fn deps => fn (_, task) => - (case task of - Task (parents, body) => - let - val result = body (task_parents deps parents); - val _ = Par_Exn.release_all (join_theory result); - val _ = result_present result (); - val _ = result_commit result (); - in result_theory result end - | Finished thy => thy)) #> ignore; - -val schedule_futures = Thread_Attributes.uninterruptible (fn _ => fn tasks => - let - val futures = tasks - |> String_Graph.schedule (fn deps => fn (name, task) => - (case task of - Task (parents, body) => - (singleton o Future.forks) - {name = "theory:" ^ name, group = NONE, - deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true} - (fn () => - (case filter (not o can Future.join o #2) deps of - [] => body (map (result_theory o Future.join) (task_parents deps parents)) - | bad => - error - ("Failed to load theory " ^ quote name ^ - " (unresolved " ^ commas_quote (map #1 bad) ^ ")"))) - | Finished theory => Future.value (theory_result theory))); - - val results1 = futures - |> maps (fn future => - (case Future.join_result future of - Exn.Res result => join_theory result - | Exn.Exn exn => [Exn.Exn exn])); - - val results2 = futures - |> map_filter (Exn.get_res o Future.join_result) - |> sort result_ord - |> Par_List.map (fn result => Exn.capture (result_present result) ()); - - (* FIXME more precise commit order (!?) *) - val results3 = futures - |> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ()); - - (* FIXME avoid global Execution.reset (!??) *) - val results4 = map Exn.Exn (maps Task_Queue.group_status (Execution.reset ())); - - val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4); - in () end); - - -(* eval theory *) - -fun excursion keywords master_dir last_timing init elements = - let - fun prepare_span st span = - Command_Span.content span - |> Command.read keywords (Command.read_thy st) master_dir init ([], ~1) - |> (fn tr => Toplevel.put_timing (last_timing tr) tr); - - fun element_result span_elem (st, _) = - let - val elem = Thy_Syntax.map_element (prepare_span st) span_elem; - val (results, st') = Toplevel.element_result keywords elem st; - val pos' = Toplevel.pos_of (Thy_Syntax.last_element elem); - in (results, (st', pos')) end; - - val (results, (end_state, end_pos)) = - fold_map element_result elements (Toplevel.toplevel, Position.none); - - val thy = Toplevel.end_theory end_pos end_state; - in (results, thy) end; - -fun eval_thy (context: context) update_time master_dir header text_pos text parents = - let - val {options, symbols, bibtex_entries, last_timing} = context; - val (name, _) = #name header; - val keywords = - fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents - (Keyword.add_keywords (#keywords header) Keyword.empty_keywords); - - val _ = writeln "eval_thy 1"; - - val spans = Outer_Syntax.parse_spans (Token.explode keywords text_pos text); - val _ = writeln "eval_thy 2"; - val elements = Thy_Syntax.parse_elements keywords spans; - val _ = writeln "eval_thy 3"; - - fun init () = - Resources.begin_theory master_dir header parents - |> Present.begin_theory bibtex_entries update_time - (fn () => implode (map (HTML.present_span symbols keywords) spans)); - - val (results, thy) = - cond_timeit true ("theory " ^ quote name) - (fn () => excursion keywords master_dir last_timing init elements); - - fun present () = - let - val _ = writeln "eval_thy 4 - present" - val segments = (spans ~~ maps Toplevel.join_results results) - |> map (fn (span, (tr, st')) => {span = span, command = tr, state = st'}); - - val X = if null segments then (writeln "eval_thy 5 - no segments";[]) - else List.concat(map (fn X => Command_Span.content (#span X)) segments) - val Y = (String.concatWith "::") (map Token.content_of X) - val _ = writeln("eval_thy 5 BEGIN\n"^Y^"eval_thy 6 END:"^Context.theory_name thy^"\n") - - val context: presentation_context = - {options = options, file_pos = text_pos, adjust_pos = I, segments = segments}; - in apply_presentation context thy end; - in (thy, present, size text) end; - - -(* require_thy -- checking database entries wrt. the file-system *) - -local - -fun required_by _ [] = "" - | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")"; - -fun load_thy context initiators update_time deps text (name, pos) keywords parents = - let - val _ = remove_thy name; - val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators); - val _ = Output.try_protocol_message (Markup.loading_theory name) []; - - val {master = (thy_path, _), imports} = deps; - val dir = Path.dir thy_path; - val header = Thy_Header.make (name, pos) imports keywords; - - val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents); - - val exec_id = Document_ID.make (); - val _ = - Execution.running Document_ID.none exec_id [] orelse - raise Fail ("Failed to register execution: " ^ Document_ID.print exec_id); - - val timing_start = Timing.start (); - - val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path); - val (theory, present, weight) = - eval_thy context update_time dir header text_pos text - (if name = Context.PureN then [Context.the_global_context ()] else parents); - - val timing_result = Timing.result timing_start; - val timing_props = [Markup.theory_timing, (Markup.nameN, name)]; - val _ = Output.try_protocol_message (timing_props @ Markup.timing_properties timing_result) [] - - fun commit () = update_thy deps theory; - in - Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight} - end; - -fun check_deps dir name = - (case lookup_deps name of - SOME NONE => (true, NONE, Position.none, get_imports name, []) - | NONE => - let val {master, text, theory_pos, imports, keywords} = Resources.check_thy dir name - in (false, SOME (make_deps master imports, text), theory_pos, imports, keywords) end - | SOME (SOME {master, ...}) => - let - val {master = master', text = text', theory_pos = theory_pos', imports = imports', - keywords = keywords'} = Resources.check_thy dir name; - val deps' = SOME (make_deps master' imports', text'); - val current = - #2 master = #2 master' andalso - (case lookup_theory name of - NONE => false - | SOME theory => Resources.loaded_files_current theory); - in (current, deps', theory_pos', imports', keywords') end); - -in - -fun require_thys context initiators qualifier dir strs tasks = - fold_map (require_thy context initiators qualifier dir) strs tasks |>> forall I -and require_thy context initiators qualifier dir (s, require_pos) tasks = - let - val {master_dir, theory_name, ...} = Resources.import_name qualifier dir s; - in - (case try (String_Graph.get_node tasks) theory_name of - SOME task => (task_finished task, tasks) - | NONE => - let - val _ = member (op =) initiators theory_name andalso error (cycle_msg initiators); - - val (current, deps, theory_pos, imports, keywords) = check_deps master_dir theory_name - handle ERROR msg => - cat_error msg - ("The error(s) above occurred for theory " ^ quote theory_name ^ - Position.here require_pos ^ required_by "\n" initiators); - - val qualifier' = Resources.theory_qualifier theory_name; - val dir' = Path.append dir (master_dir_deps (Option.map #1 deps)); - - val parents = map (#theory_name o Resources.import_name qualifier' dir' o #1) imports; - val (parents_current, tasks') = - require_thys context (theory_name :: initiators) qualifier' dir' imports tasks; - - val all_current = current andalso parents_current; - val task = - if all_current then Finished (get_theory theory_name) - else - (case deps of - NONE => raise Fail "Malformed deps" - | SOME (dep, text) => - let - val update_time = serial (); - val load = - load_thy context initiators update_time - dep text (theory_name, theory_pos) keywords; - in Task (parents, load) end); - - val tasks'' = new_entry theory_name parents task tasks'; - in (all_current, tasks'') end) - end; - -end; - - -(* use theories *) - -fun use_theories context qualifier master_dir imports = - let val (_, tasks) = require_thys context [] qualifier master_dir imports String_Graph.empty - in if Multithreading.max_threads () > 1 then schedule_futures tasks else schedule_seq tasks end; - -fun use_thy name = - use_theories (default_context ()) Resources.default_qualifier - Path.current [(name, Position.none)]; - - -(* toplevel scripting -- without maintaining database *) - -fun script_thy pos txt thy = - let - val trs = - Outer_Syntax.parse thy pos txt - |> map (Toplevel.modify_init (K thy)); - val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs); - val end_state = fold (Toplevel.command_exception true) trs Toplevel.toplevel; - in Toplevel.end_theory end_pos end_state end; - - -(* register theory *) - -fun register_thy theory = - let - val name = Context.theory_long_name theory; - val {master, ...} = Resources.check_thy (Resources.master_directory theory) name; - val imports = Resources.imports_of theory; - in - change_thys (fn thys => - let - val thys' = remove name thys; - val _ = writeln ("Registering theory " ^ quote name); - in update (make_deps master imports) theory thys' end) - end; - - -(* finish all theories *) - -fun finish () = change_thys (String_Graph.map (fn _ => fn (_, entry) => (NONE, entry))); - -end; - -fun use_thy name = Runtime.toplevel_program (fn () => Thy_Info.use_thy name); diff --git a/src/patches/thy_info.orig.ML b/src/patches/thy_info.orig.ML deleted file mode 100644 index ee4855da..00000000 --- a/src/patches/thy_info.orig.ML +++ /dev/null @@ -1,484 +0,0 @@ -(* Title: Pure/Thy/thy_info.ML - Author: Markus Wenzel, TU Muenchen - -Global theory info database, with auto-loading according to theory and -file dependencies. -*) - -signature THY_INFO = -sig - type presentation_context = - {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T, - segments: Thy_Output.segment list} - val apply_presentation: presentation_context -> theory -> unit - val add_presentation: (presentation_context -> theory -> unit) -> theory -> theory - val get_names: unit -> string list - val lookup_theory: string -> theory option - val get_theory: string -> theory - val master_directory: string -> Path.T - val remove_thy: string -> unit - type context = - {options: Options.T, - symbols: HTML.symbols, - bibtex_entries: string list, - last_timing: Toplevel.transition -> Time.time} - val use_theories: context -> string -> Path.T -> (string * Position.T) list -> unit - val use_thy: string -> unit - val script_thy: Position.T -> string -> theory -> theory - val register_thy: theory -> unit - val finish: unit -> unit -end; - -structure Thy_Info: THY_INFO = -struct - -(** presentation of consolidated theory **) - -type presentation_context = - {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T, - segments: Thy_Output.segment list}; - -structure Presentation = Theory_Data -( - type T = ((presentation_context -> theory -> unit) * stamp) list; - val empty = []; - val extend = I; - fun merge data : T = Library.merge (eq_snd op =) data; -); - -fun apply_presentation (context: presentation_context) thy = - ignore (Presentation.get thy |> Par_List.map (fn (f, _) => f context thy)); - -fun add_presentation f = Presentation.map (cons (f, stamp ())); - -val _ = - Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy => - if exists (Toplevel.is_skipped_proof o #state) segments then () - else - let - val body = Thy_Output.present_thy options thy segments; - val option = Present.document_option options; - in - if #disabled option then () - else - let - val latex = Latex.isabelle_body (Context.theory_name thy) body; - val output = [Latex.output_text latex, Latex.output_positions file_pos latex]; - val _ = - if Options.bool options "export_document" - then Export.export thy "document.tex" output else (); - val _ = if #enabled option then Present.theory_output thy output else (); - in () end - end)); - - - -(** thy database **) - -(* messages *) - -val show_path = space_implode " via " o map quote; - -fun cycle_msg names = "Cyclic dependency of " ^ show_path names; - - -(* derived graph operations *) - -fun add_deps name parents G = String_Graph.add_deps_acyclic (name, parents) G - handle String_Graph.CYCLES namess => error (cat_lines (map cycle_msg namess)); - -fun new_entry name parents entry = - String_Graph.new_node (name, entry) #> add_deps name parents; - - -(* global thys *) - -type deps = - {master: (Path.T * SHA1.digest), (*master dependencies for thy file*) - imports: (string * Position.T) list}; (*source specification of imports (partially qualified)*) - -fun make_deps master imports : deps = {master = master, imports = imports}; - -fun master_dir_deps (d: deps option) = - the_default Path.current (Option.map (Path.dir o #1 o #master) d); - -local - val global_thys = - Synchronized.var "Thy_Info.thys" - (String_Graph.empty: (deps option * theory option) String_Graph.T); -in - fun get_thys () = Synchronized.value global_thys; - fun change_thys f = Synchronized.change global_thys f; -end; - -fun get_names () = String_Graph.topological_order (get_thys ()); - - -(* access thy *) - -fun lookup thys name = try (String_Graph.get_node thys) name; -fun lookup_thy name = lookup (get_thys ()) name; - -fun get thys name = - (case lookup thys name of - SOME thy => thy - | NONE => error ("Theory loader: nothing known about theory " ^ quote name)); - -fun get_thy name = get (get_thys ()) name; - - -(* access deps *) - -val lookup_deps = Option.map #1 o lookup_thy; - -val master_directory = master_dir_deps o #1 o get_thy; - - -(* access theory *) - -fun lookup_theory name = - (case lookup_thy name of - SOME (_, SOME theory) => SOME theory - | _ => NONE); - -fun get_theory name = - (case lookup_theory name of - SOME theory => theory - | _ => error ("Theory loader: undefined entry for theory " ^ quote name)); - -val get_imports = Resources.imports_of o get_theory; - - - -(** thy operations **) - -(* remove *) - -fun remove name thys = - (case lookup thys name of - NONE => thys - | SOME (NONE, _) => error ("Cannot update finished theory " ^ quote name) - | SOME _ => - let - val succs = String_Graph.all_succs thys [name]; - val _ = writeln ("Theory loader: removing " ^ commas_quote succs); - in fold String_Graph.del_node succs thys end); - -val remove_thy = change_thys o remove; - - -(* update *) - -fun update deps theory thys = - let - val name = Context.theory_long_name theory; - val parents = map Context.theory_long_name (Theory.parents_of theory); - - val thys' = remove name thys; - val _ = map (get thys') parents; - in new_entry name parents (SOME deps, SOME theory) thys' end; - -fun update_thy deps theory = change_thys (update deps theory); - - -(* context *) - -type context = - {options: Options.T, - symbols: HTML.symbols, - bibtex_entries: string list, - last_timing: Toplevel.transition -> Time.time}; - -fun default_context (): context = - {options = Options.default (), - symbols = HTML.no_symbols, - bibtex_entries = [], - last_timing = K Time.zeroTime}; - - -(* scheduling loader tasks *) - -datatype result = - Result of {theory: theory, exec_id: Document_ID.exec, - present: unit -> unit, commit: unit -> unit, weight: int}; - -fun theory_result theory = - Result {theory = theory, exec_id = Document_ID.none, present = I, commit = I, weight = 0}; - -fun result_theory (Result {theory, ...}) = theory; -fun result_present (Result {present, ...}) = present; -fun result_commit (Result {commit, ...}) = commit; -fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i); - -fun join_theory (Result {theory, exec_id, ...}) = - let - val _ = Execution.join [exec_id]; - val res = Exn.capture Thm.consolidate_theory theory; - val exns = maps Task_Queue.group_status (Execution.peek exec_id); - in res :: map Exn.Exn exns end; - -datatype task = - Task of string list * (theory list -> result) | - Finished of theory; - -fun task_finished (Task _) = false - | task_finished (Finished _) = true; - -fun task_parents deps (parents: string list) = map (the o AList.lookup (op =) deps) parents; - -val schedule_seq = - String_Graph.schedule (fn deps => fn (_, task) => - (case task of - Task (parents, body) => - let - val result = body (task_parents deps parents); - val _ = Par_Exn.release_all (join_theory result); - val _ = result_present result (); - val _ = result_commit result (); - in result_theory result end - | Finished thy => thy)) #> ignore; - -val schedule_futures = Thread_Attributes.uninterruptible (fn _ => fn tasks => - let - val futures = tasks - |> String_Graph.schedule (fn deps => fn (name, task) => - (case task of - Task (parents, body) => - (singleton o Future.forks) - {name = "theory:" ^ name, group = NONE, - deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true} - (fn () => - (case filter (not o can Future.join o #2) deps of - [] => body (map (result_theory o Future.join) (task_parents deps parents)) - | bad => - error - ("Failed to load theory " ^ quote name ^ - " (unresolved " ^ commas_quote (map #1 bad) ^ ")"))) - | Finished theory => Future.value (theory_result theory))); - - val results1 = futures - |> maps (fn future => - (case Future.join_result future of - Exn.Res result => join_theory result - | Exn.Exn exn => [Exn.Exn exn])); - - val results2 = futures - |> map_filter (Exn.get_res o Future.join_result) - |> sort result_ord - |> Par_List.map (fn result => Exn.capture (result_present result) ()); - - (* FIXME more precise commit order (!?) *) - val results3 = futures - |> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ()); - - (* FIXME avoid global Execution.reset (!??) *) - val results4 = map Exn.Exn (maps Task_Queue.group_status (Execution.reset ())); - - val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4); - in () end); - - -(* eval theory *) - -fun excursion keywords master_dir last_timing init elements = - let - fun prepare_span st span = - Command_Span.content span - |> Command.read keywords (Command.read_thy st) master_dir init ([], ~1) - |> (fn tr => Toplevel.put_timing (last_timing tr) tr); - - fun element_result span_elem (st, _) = - let - val elem = Thy_Syntax.map_element (prepare_span st) span_elem; - val (results, st') = Toplevel.element_result keywords elem st; - val pos' = Toplevel.pos_of (Thy_Syntax.last_element elem); - in (results, (st', pos')) end; - - val (results, (end_state, end_pos)) = - fold_map element_result elements (Toplevel.toplevel, Position.none); - - val thy = Toplevel.end_theory end_pos end_state; - in (results, thy) end; - -fun eval_thy (context: context) update_time master_dir header text_pos text parents = - let - val {options, symbols, bibtex_entries, last_timing} = context; - val (name, _) = #name header; - val keywords = - fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents - (Keyword.add_keywords (#keywords header) Keyword.empty_keywords); - - val spans = Outer_Syntax.parse_spans (Token.explode keywords text_pos text); - val elements = Thy_Syntax.parse_elements keywords spans; - - fun init () = - Resources.begin_theory master_dir header parents - |> Present.begin_theory bibtex_entries update_time - (fn () => implode (map (HTML.present_span symbols keywords) spans)); - - val (results, thy) = - cond_timeit true ("theory " ^ quote name) - (fn () => excursion keywords master_dir last_timing init elements); - - fun present () = - let - val segments = (spans ~~ maps Toplevel.join_results results) - |> map (fn (span, (tr, st')) => {span = span, command = tr, state = st'}); - val context: presentation_context = - {options = options, file_pos = text_pos, adjust_pos = I, segments = segments}; - in apply_presentation context thy end; - in (thy, present, size text) end; - - -(* require_thy -- checking database entries wrt. the file-system *) - -local - -fun required_by _ [] = "" - | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")"; - -fun load_thy context initiators update_time deps text (name, pos) keywords parents = - let - val _ = remove_thy name; - val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators); - val _ = Output.try_protocol_message (Markup.loading_theory name) []; - - val {master = (thy_path, _), imports} = deps; - val dir = Path.dir thy_path; - val header = Thy_Header.make (name, pos) imports keywords; - - val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents); - - val exec_id = Document_ID.make (); - val _ = - Execution.running Document_ID.none exec_id [] orelse - raise Fail ("Failed to register execution: " ^ Document_ID.print exec_id); - - val timing_start = Timing.start (); - - val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path); - val (theory, present, weight) = - eval_thy context update_time dir header text_pos text - (if name = Context.PureN then [Context.the_global_context ()] else parents); - - val timing_result = Timing.result timing_start; - val timing_props = [Markup.theory_timing, (Markup.nameN, name)]; - val _ = Output.try_protocol_message (timing_props @ Markup.timing_properties timing_result) [] - - fun commit () = update_thy deps theory; - in - Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight} - end; - -fun check_deps dir name = - (case lookup_deps name of - SOME NONE => (true, NONE, Position.none, get_imports name, []) - | NONE => - let val {master, text, theory_pos, imports, keywords} = Resources.check_thy dir name - in (false, SOME (make_deps master imports, text), theory_pos, imports, keywords) end - | SOME (SOME {master, ...}) => - let - val {master = master', text = text', theory_pos = theory_pos', imports = imports', - keywords = keywords'} = Resources.check_thy dir name; - val deps' = SOME (make_deps master' imports', text'); - val current = - #2 master = #2 master' andalso - (case lookup_theory name of - NONE => false - | SOME theory => Resources.loaded_files_current theory); - in (current, deps', theory_pos', imports', keywords') end); - -in - -fun require_thys context initiators qualifier dir strs tasks = - fold_map (require_thy context initiators qualifier dir) strs tasks |>> forall I -and require_thy context initiators qualifier dir (s, require_pos) tasks = - let - val {master_dir, theory_name, ...} = Resources.import_name qualifier dir s; - in - (case try (String_Graph.get_node tasks) theory_name of - SOME task => (task_finished task, tasks) - | NONE => - let - val _ = member (op =) initiators theory_name andalso error (cycle_msg initiators); - - val (current, deps, theory_pos, imports, keywords) = check_deps master_dir theory_name - handle ERROR msg => - cat_error msg - ("The error(s) above occurred for theory " ^ quote theory_name ^ - Position.here require_pos ^ required_by "\n" initiators); - - val qualifier' = Resources.theory_qualifier theory_name; - val dir' = Path.append dir (master_dir_deps (Option.map #1 deps)); - - val parents = map (#theory_name o Resources.import_name qualifier' dir' o #1) imports; - val (parents_current, tasks') = - require_thys context (theory_name :: initiators) qualifier' dir' imports tasks; - - val all_current = current andalso parents_current; - val task = - if all_current then Finished (get_theory theory_name) - else - (case deps of - NONE => raise Fail "Malformed deps" - | SOME (dep, text) => - let - val update_time = serial (); - val load = - load_thy context initiators update_time - dep text (theory_name, theory_pos) keywords; - in Task (parents, load) end); - - val tasks'' = new_entry theory_name parents task tasks'; - in (all_current, tasks'') end) - end; - -end; - - -(* use theories *) - -fun use_theories context qualifier master_dir imports = - let val (_, tasks) = require_thys context [] qualifier master_dir imports String_Graph.empty - in if Multithreading.max_threads () > 1 then schedule_futures tasks else schedule_seq tasks end; - -fun use_thy name = - use_theories (default_context ()) Resources.default_qualifier - Path.current [(name, Position.none)]; - - -(* toplevel scripting -- without maintaining database *) - -fun script_thy pos txt thy = - let - val trs = - Outer_Syntax.parse thy pos txt - |> map (Toplevel.modify_init (K thy)); - val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs); - val end_state = fold (Toplevel.command_exception true) trs Toplevel.toplevel; - in Toplevel.end_theory end_pos end_state end; - - -(* register theory *) - -fun register_thy theory = - let - val name = Context.theory_long_name theory; - val {master, ...} = Resources.check_thy (Resources.master_directory theory) name; - val imports = Resources.imports_of theory; - in - change_thys (fn thys => - let - val thys' = remove name thys; - val _ = writeln ("Registering theory " ^ quote name); - in update (make_deps master imports) theory thys' end) - end; - - -(* finish all theories *) - -fun finish () = change_thys (String_Graph.map (fn _ => fn (_, entry) => (NONE, entry))); - -end; - -fun use_thy name = Runtime.toplevel_program (fn () => Thy_Info.use_thy name); From 0c41ee46bb6de10b12b6358e72b33e299f9d6f35 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Wed, 8 Apr 2020 13:12:17 +0100 Subject: [PATCH 2/7] Port to Isabelle 2020 (tested with Isabelle 2020 RC4). --- .../TR_MyCommentedIsabelle.thy | 9 ++- src/DOF/Assert.thy | 2 +- src/ROOT | 17 ++++++ src/ROOTS | 1 + ...t.orig19.ML => thy_output.Isabelle2020.ML} | 54 +++++++++--------- src/patches/thy_output.ML | 56 ++++++++++--------- src/tests/AssnsLemmaThmEtc.thy | 4 +- src/tests/Attributes.thy | 2 +- src/tests/Concept_Example.thy | 4 +- src/tests/Concept_ExampleInvariant.thy | 2 +- src/tests/InnerSyntaxAntiquotations.thy | 2 +- src/tests/ROOT | 8 +++ 12 files changed, 94 insertions(+), 67 deletions(-) create mode 100644 src/ROOTS rename src/patches/{thy_output.orig19.ML => thy_output.Isabelle2020.ML} (93%) create mode 100644 src/tests/ROOT diff --git a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy index 0e2b65aa..f38b6b98 100644 --- a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy +++ b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy @@ -14,7 +14,6 @@ (*<*) theory TR_MyCommentedIsabelle imports "Isabelle_DOF.technical_report" - (*imports "../../../ontologies/technical_report"*) begin @@ -784,9 +783,9 @@ Theory.setup: (theory -> theory) -> unit; (* The thing to extend the table of " Theory.get_markup: theory -> Markup.T; Theory.axiom_table: theory -> term Name_Space.table; Theory.axiom_space: theory -> Name_Space.T; -Theory.axioms_of: theory -> (string * term) list; Theory.all_axioms_of: theory -> (string * term) list; Theory.defs_of: theory -> Defs.T; +Theory.join_theory: theory list -> theory; Theory.at_begin: (theory -> theory option) -> theory -> theory; Theory.at_end: (theory -> theory option) -> theory -> theory; Theory.begin_theory: string * Position.T -> theory list -> theory; @@ -1016,7 +1015,7 @@ fun derive_thm name term lthy = [] (* local assumption context *) (term) (* parsed goal *) (fn _ => simp_tac lthy 1) (* proof tactic *) - |> Thm.close_derivation (* some cleanups *); + |> Thm.close_derivation \<^here> (* some cleanups *); val thm111_intern = derive_thm "thm111" tt @{context} (* just for fun at the ML level *) @@ -1035,7 +1034,7 @@ text\Converting a local theory transformation into a global one:\ setup\SimpleSampleProof.prove_n_store\ text\... and there it is in the global (Isar) context:\ -thm thm111 +thm "thm111" @@ -2038,7 +2037,7 @@ text\The heart of the LaTeX generator is to be found in the structure @{ML \ ML\ -local +local open Latex diff --git a/src/DOF/Assert.thy b/src/DOF/Assert.thy index cb98e3d9..84b7e9e8 100644 --- a/src/DOF/Assert.thy +++ b/src/DOF/Assert.thy @@ -48,7 +48,7 @@ fun assert_cmd some_name modes raw_t ctxt (* state*) = val ty' = Term.type_of t'; val ty' = case ty' of @{typ "bool"} => ty' | _ => error "Assertion expressions must be boolean."; val t' = case t' of @{term "True"} => t' | _ => error "Assertion failed."; - val ctxt' = Variable.auto_fixes t' ctxt; + val ctxt' = Proof_Context.augment t' ctxt; val p = Print_Mode.with_modes modes (fn () => Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk, Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) (); diff --git a/src/ROOT b/src/ROOT index fbd6e312..abc6750e 100644 --- a/src/ROOT +++ b/src/ROOT @@ -2,15 +2,32 @@ session "Isabelle_DOF" = "Functional-Automata" + options [document = pdf, document_output = "output"] sessions "Regular-Sets" + directories + "DOF" + "ontologies" + "ontologies/CENELEC_50128" + "ontologies/Conceptual" + "ontologies/math_exam" + "ontologies/math_paper" + "ontologies/scholarly_paper" + "ontologies/small_math" + "ontologies/technical_report" theories "DOF/Isa_DOF" "ontologies/ontologies" + + + +(* session "Isabelle_DOF-tests" = "Isabelle_DOF" + options [document = false] + directories + tests theories "tests/AssnsLemmaThmEtc" "tests/Concept_ExampleInvariant" "tests/Concept_Example" "tests/InnerSyntaxAntiquotations" "tests/Attributes" +*) diff --git a/src/ROOTS b/src/ROOTS new file mode 100644 index 00000000..2b29f276 --- /dev/null +++ b/src/ROOTS @@ -0,0 +1 @@ +tests diff --git a/src/patches/thy_output.orig19.ML b/src/patches/thy_output.Isabelle2020.ML similarity index 93% rename from src/patches/thy_output.orig19.ML rename to src/patches/thy_output.Isabelle2020.ML index d3ec5d9e..94a67697 100644 --- a/src/patches/thy_output.orig19.ML +++ b/src/patches/thy_output.Isabelle2020.ML @@ -175,30 +175,30 @@ end; (* presentation tokens *) datatype token = - Ignore_Token - | Basic_Token of Token.T - | Markup_Token of string * Input.source - | Markup_Env_Token of string * Input.source - | Raw_Token of Input.source; + Ignore + | Token of Token.T + | Heading of string * Input.source + | Body of string * Input.source + | Raw of Input.source; -fun basic_token pred (Basic_Token tok) = pred tok - | basic_token _ _ = false; +fun token_with pred (Token tok) = pred tok + | token_with _ _ = false; -val white_token = basic_token Document_Source.is_white; -val white_comment_token = basic_token Document_Source.is_white_comment; -val blank_token = basic_token Token.is_blank; -val newline_token = basic_token Token.is_newline; +val white_token = token_with Document_Source.is_white; +val white_comment_token = token_with Document_Source.is_white_comment; +val blank_token = token_with Token.is_blank; +val newline_token = token_with Token.is_newline; fun present_token ctxt tok = (case tok of - Ignore_Token => [] - | Basic_Token tok => output_token ctxt tok - | Markup_Token (cmd, source) => + Ignore => [] + | Token tok => output_token ctxt tok + | Heading (cmd, source) => Latex.enclose_body ("%\n\\isamarkup" ^ cmd ^ "{") "%\n}\n" (output_document ctxt {markdown = false} source) - | Markup_Env_Token (cmd, source) => + | Body (cmd, source) => [Latex.environment_block ("isamarkup" ^ cmd) (output_document ctxt {markdown = true} source)] - | Raw_Token source => + | Raw source => Latex.string "%\n" :: output_document ctxt {markdown = true} source @ [Latex.string "\n"]); @@ -367,7 +367,7 @@ fun present_thy options thy (segments: segment list) = (* tokens *) val ignored = Scan.state --| ignore - >> (fn d => (NONE, (Ignore_Token, ("", d)))); + >> (fn d => (NONE, (Ignore, ("", d)))); fun markup pred mk flag = Scan.peek (fn d => Document_Source.improper |-- @@ -384,29 +384,29 @@ fun present_thy options thy (segments: segment list) = Scan.optional (Scan.one Token.is_command_modifier ::: Document_Source.improper) [] -- Scan.one Token.is_command --| Document_Source.annotation >> (fn (cmd_mod, cmd) => - map (fn tok => (NONE, (Basic_Token tok, ("", d)))) cmd_mod @ + map (fn tok => (NONE, (Token tok, ("", d)))) cmd_mod @ [(SOME (Token.content_of cmd, Token.pos_of cmd), - (Basic_Token cmd, (markup_false, d)))])); + (Token cmd, (markup_false, d)))])); val cmt = Scan.peek (fn d => - Scan.one Document_Source.is_black_comment >> (fn tok => (NONE, (Basic_Token tok, ("", d))))); + Scan.one Document_Source.is_black_comment >> (fn tok => (NONE, (Token tok, ("", d))))); val other = Scan.peek (fn d => - Parse.not_eof >> (fn tok => (NONE, (Basic_Token tok, ("", d))))); + Parse.not_eof >> (fn tok => (NONE, (Token tok, ("", d))))); val tokens = (ignored || - markup Keyword.is_document_heading Markup_Token markup_true || - markup Keyword.is_document_body Markup_Env_Token markup_true || - markup Keyword.is_document_raw (Raw_Token o #2) "") >> single || + markup Keyword.is_document_heading Heading markup_true || + markup Keyword.is_document_body Body markup_true || + markup Keyword.is_document_raw (Raw o #2) "") >> single || command || (cmt || other) >> single; (* spans *) - val is_eof = fn (_, (Basic_Token x, _)) => Token.is_eof x | _ => false; - val stopper = Scan.stopper (K (NONE, (Basic_Token Token.eof, ("", 0)))) is_eof; + val is_eof = fn (_, (Token x, _)) => Token.is_eof x | _ => false; + val stopper = Scan.stopper (K (NONE, (Token Token.eof, ("", 0)))) is_eof; val cmd = Scan.one (is_some o fst); val non_cmd = Scan.one (is_none o fst andf not o is_eof) >> #2; @@ -466,7 +466,7 @@ end; (* pretty printing *) fun pretty_term ctxt t = - Syntax.pretty_term (Variable.auto_fixes t ctxt) t; + Syntax.pretty_term (Proof_Context.augment t ctxt) t; fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of; diff --git a/src/patches/thy_output.ML b/src/patches/thy_output.ML index b0a82128..7139b13a 100644 --- a/src/patches/thy_output.ML +++ b/src/patches/thy_output.ML @@ -2,6 +2,8 @@ Author: Makarius Theory document output. + +This is a modified/patched version that supports Isabelle/DOF. *) signature THY_OUTPUT = @@ -176,32 +178,32 @@ end; (* presentation tokens *) datatype token = - Ignore_Token - | Basic_Token of Token.T - | Markup_Token of string * string * Input.source - | Markup_Env_Token of string * string * Input.source - | Raw_Token of Input.source; + Ignore + | Token of Token.T + | Heading of string * string * Input.source + | Body of string * string * Input.source + | Raw of Input.source; -fun basic_token pred (Basic_Token tok) = pred tok - | basic_token _ _ = false; +fun token_with pred (Token tok) = pred tok + | token_with _ _ = false; -val white_token = basic_token Document_Source.is_white; -val white_comment_token = basic_token Document_Source.is_white_comment; -val blank_token = basic_token Token.is_blank; -val newline_token = basic_token Token.is_newline; +val white_token = token_with Document_Source.is_white; +val white_comment_token = token_with Document_Source.is_white_comment; +val blank_token = token_with Token.is_blank; +val newline_token = token_with Token.is_newline; fun present_token ctxt tok = (case tok of - Ignore_Token => [] - | Basic_Token tok => output_token ctxt tok - | Markup_Token (cmd, meta_args, source) => + Ignore => [] + | Token tok => output_token ctxt tok + | Heading (cmd, meta_args, source) => Latex.enclose_body ("%\n\\isamarkup" ^ cmd (* ^ meta_args *) ^ "{") "%\n}\n" (output_document ctxt {markdown = false} source) - | Markup_Env_Token (cmd, meta_args, source) => + | Body (cmd, meta_args, source) => [Latex.environment_block ("isamarkup" ^ cmd (* ^ meta_args*)) (Latex.string meta_args :: output_document ctxt {markdown = true} source)] - | Raw_Token source => + | Raw source => Latex.string "%\n" :: output_document ctxt {markdown = true} source @ [Latex.string "\n"]); @@ -376,7 +378,7 @@ fun present_thy options thy (segments: segment list) = (* tokens *) val ignored = Scan.state --| ignore - >> (fn d => (NONE, (Ignore_Token, ("", d)))); + >> (fn d => (NONE, (Ignore, ("", d)))); fun markup pred mk flag = Scan.peek (fn d => Document_Source.improper @@ -399,29 +401,29 @@ fun present_thy options thy (segments: segment list) = Scan.optional (Scan.one Token.is_command_modifier ::: Document_Source.improper) [] -- Scan.one Token.is_command --| Document_Source.annotation >> (fn (cmd_mod, cmd) => - map (fn tok => (NONE, (Basic_Token tok, ("", d)))) cmd_mod @ + map (fn tok => (NONE, (Token tok, ("", d)))) cmd_mod @ [(SOME (Token.content_of cmd, Token.pos_of cmd), - (Basic_Token cmd, (markup_false, d)))])); + (Token cmd, (markup_false, d)))])); val cmt = Scan.peek (fn d => - Scan.one Document_Source.is_black_comment >> (fn tok => (NONE, (Basic_Token tok, ("", d))))); + Scan.one Document_Source.is_black_comment >> (fn tok => (NONE, (Token tok, ("", d))))); val other = Scan.peek (fn d => - Parse.not_eof >> (fn tok => (NONE, (Basic_Token tok, ("", d))))); + Parse.not_eof >> (fn tok => (NONE, (Token tok, ("", d))))); val tokens = (ignored || - markup Keyword.is_document_heading Markup_Token markup_true || - markup Keyword.is_document_body Markup_Env_Token markup_true || - markup Keyword.is_document_raw (Raw_Token o #3) "") >> single || + markup Keyword.is_document_heading Heading markup_true || + markup Keyword.is_document_body Body markup_true || + markup Keyword.is_document_raw (Raw o #3) "") >> single || command || (cmt || other) >> single; (* spans *) - val is_eof = fn (_, (Basic_Token x, _)) => Token.is_eof x | _ => false; - val stopper = Scan.stopper (K (NONE, (Basic_Token Token.eof, ("", 0)))) is_eof; + val is_eof = fn (_, (Token x, _)) => Token.is_eof x | _ => false; + val stopper = Scan.stopper (K (NONE, (Token Token.eof, ("", 0)))) is_eof; val cmd = Scan.one (is_some o fst); val non_cmd = Scan.one (is_none o fst andf not o is_eof) >> #2; @@ -488,7 +490,7 @@ end; (* pretty printing *) fun pretty_term ctxt t = - Syntax.pretty_term (Variable.auto_fixes t ctxt) t; + Syntax.pretty_term (Proof_Context.augment t ctxt) t; fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of; diff --git a/src/tests/AssnsLemmaThmEtc.thy b/src/tests/AssnsLemmaThmEtc.thy index c822d21c..ab710728 100644 --- a/src/tests/AssnsLemmaThmEtc.thy +++ b/src/tests/AssnsLemmaThmEtc.thy @@ -14,8 +14,8 @@ theory AssnsLemmaThmEtc imports - "../ontologies/Conceptual/Conceptual" - "../ontologies/math_paper/math_paper" + "Isabelle_DOF.Conceptual" + "Isabelle_DOF.math_paper" begin section\Elementary Creation of Doc-items and Access of their Attibutes\ diff --git a/src/tests/Attributes.thy b/src/tests/Attributes.thy index 426a53ec..72bda2dc 100644 --- a/src/tests/Attributes.thy +++ b/src/tests/Attributes.thy @@ -14,7 +14,7 @@ theory Attributes imports - "../ontologies/Conceptual/Conceptual" + "Isabelle_DOF.Conceptual" begin section\Elementary Creation of Doc-items and Access of their Attibutes\ diff --git a/src/tests/Concept_Example.thy b/src/tests/Concept_Example.thy index a6e18fce..95a8d44e 100644 --- a/src/tests/Concept_Example.thy +++ b/src/tests/Concept_Example.thy @@ -16,10 +16,10 @@ chapter\Setting and modifying attributes of doc-items\ theory Concept_Example imports - "../ontologies/Conceptual/Conceptual" (* we use the generic "Conceptual" ontology *) + "Isabelle_DOF.Conceptual" (* we use the generic "Conceptual" ontology *) begin -text\@{theory "Isabelle_DOF-tests.Conceptual"} provides a monitor @{typ M} enforcing a particular document structure. +text\@{theory "Isabelle_DOF.Conceptual"} provides a monitor @{typ M} enforcing a particular document structure. Here, we say: From now on, this structural rules are respected wrt. all doc\_classes M is enabled for.\ open_monitor*[struct::M] diff --git a/src/tests/Concept_ExampleInvariant.thy b/src/tests/Concept_ExampleInvariant.thy index b117105e..7fd00c0d 100644 --- a/src/tests/Concept_ExampleInvariant.thy +++ b/src/tests/Concept_ExampleInvariant.thy @@ -16,7 +16,7 @@ chapter\Setting and modifying attributes of doc-items\ theory Concept_ExampleInvariant imports - "../ontologies/Conceptual/Conceptual" (* we use the generic "Conceptual" ontology *) + "Isabelle_DOF.Conceptual" (* we use the generic "Conceptual" ontology *) begin section\Example: Standard Class Invariant\ diff --git a/src/tests/InnerSyntaxAntiquotations.thy b/src/tests/InnerSyntaxAntiquotations.thy index 34b8bcf1..fe1a73a3 100644 --- a/src/tests/InnerSyntaxAntiquotations.thy +++ b/src/tests/InnerSyntaxAntiquotations.thy @@ -16,7 +16,7 @@ chapter\Inner Syntax Antiquotations (ISA)'s\ theory InnerSyntaxAntiquotations imports - "../ontologies/Conceptual/Conceptual" + "Isabelle_DOF.Conceptual" begin text\Since the syntax chosen for values of doc-class attributes is HOL-syntax --- requiring diff --git a/src/tests/ROOT b/src/tests/ROOT new file mode 100644 index 00000000..f4296709 --- /dev/null +++ b/src/tests/ROOT @@ -0,0 +1,8 @@ +session "Isabelle_DOF-tests" = "Isabelle_DOF" + + options [document = false] + theories + "AssnsLemmaThmEtc" + "Concept_ExampleInvariant" + "Concept_Example" + "InnerSyntaxAntiquotations" + "Attributes" From f13e325f6aacba4aac6c31c9b96a14866b52d952 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Wed, 8 Apr 2020 13:19:32 +0100 Subject: [PATCH 3/7] Port to Isabelle 2020 (tested with Isabelle 2020 RC4). --- README.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index c907734a..4a69d296 100644 --- a/README.md +++ b/README.md @@ -20,9 +20,9 @@ foo@bar:~$ docker run -ti --rm -e DISPLAY=$DISPLAY -v /tmp/.X11-unix:/tmp/.X11-u Isabelle/DOF has two major pre-requisites: -* **Isabelle:** Isabelle/DOF requires [Isabelle 2019](http://isabelle.in.tum.de/website-Isabelle2019/). +* **Isabelle:** Isabelle/DOF requires [Isabelle 2020](http://isabelle.in.tum.de/website-Isabelle2020-RC4/). Please download the Isabelle 2019 distribution for your operating - system from the [Isabelle website](http://isabelle.in.tum.de/website-Isabelle2019/). + system from the [Isabelle website](http://isabelle.in.tum.de/website-Isabelle2020-RC4/). * **LaTeX:** Isabelle/DOF requires a modern pdfTeX-engine supporting the \expanded{}-primitive. This is, for example, included in the [TeXLive 2019](https://www.tug.org/texlive/) (or later) distribution. Please follow the [TeXLive installation instructions](https://www.tug.org/texlive/acquire-netinstall.html) @@ -41,7 +41,7 @@ one), the full path to the ``isabelle`` command needs to be passed as using the ``--isabelle`` command line argument of the ``install`` script: ```console -foo@bar:~$ ./install --isabelle /usr/local/Isabelle2019/bin/isabelle +foo@bar:~$ ./install --isabelle /usr/local/Isabelle2020-RC4/bin/isabelle ``` For further command line options of the installer, please use the From 968694f153c74e160f1a7fce7c7143f0e560506b Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Wed, 8 Apr 2020 16:26:00 +0100 Subject: [PATCH 4/7] Port to Isabelle 2020 (tested with Isabelle 2020 RC4). --- .config | 6 +++--- install | 6 ++++-- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/.config b/.config index ead59509..d0c9a9f8 100644 --- a/.config +++ b/.config @@ -6,9 +6,9 @@ DOF_LATEST_DOI="10.5281/zenodo.3370483" DOF_GENERIC_DOI="10.5281/zenodo.3370482" # # Isabelle and AFP Configuration -ISABELLE_VERSION="Isabelle2019: June 2019" -ISABELLE_URL="https://isabelle.in.tum.de/website-Isabelle2019/" -AFP_DATE="afp-2019-06-17" +ISABELLE_VERSION="Isabelle2020-RC4: April 2020" +ISABELLE_URL="https://isabelle.in.tum.de/website-Isabelle2020-RC4/" +AFP_DATE="afp-2020-04-17" AFP_URL="https://www.isa-afp.org/release/"$AFP_DATE".tar.gz" # # Isabelle/DOF Repository Configuration diff --git a/install b/install index 4d05efd6..4f1ff079 100755 --- a/install +++ b/install @@ -1,7 +1,7 @@ #!/usr/bin/env bash # Copyright (c) 2018-2019 The University of Sheffield. -# 2019-2019 The University of Exeter. -# 2018-2019 The University of Paris-Saclay. +# 2019-2020 The University of Exeter. +# 2018-2020 The University of Paris-Saclay. # # Redistribution and use in source and binary forms, with or without # modification, are permitted provided that the following conditions @@ -126,6 +126,8 @@ check_afp_entries() { fi done if [ "$missing" != "" ]; then + echo " Please install development version of AFP for Isabelle 2020 manually." + exit_error echo " Trying to install AFP (this might take a few *minutes*) ...." extract="" for e in $missing; do From 358be52b6191e73ac42a957b2bc5871dc768c9d5 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Wed, 8 Apr 2020 21:40:34 +0100 Subject: [PATCH 5/7] Updated Isabelle version. --- README.md | 2 +- .../Isabelle_DOF-Manual/03_GuidedTour.thy | 6 +++--- .../Isabelle_DOF-Manual/04_RefMan.thy | 18 +++++++++--------- .../Isabelle_DOF-Manual/05_Implementation.thy | 2 +- .../Isabelle_DOF-Manual/document/root.bib | 18 +++++++++--------- .../TR_MyCommentedIsabelle.thy | 2 +- .../CENELEC_50128/DOF-CENELEC_50128.sty | 2 +- .../scholarly_paper/DOF-scholarly_paper.sty | 2 +- 8 files changed, 26 insertions(+), 26 deletions(-) diff --git a/README.md b/README.md index 4a69d296..96c2bbea 100644 --- a/README.md +++ b/README.md @@ -21,7 +21,7 @@ foo@bar:~$ docker run -ti --rm -e DISPLAY=$DISPLAY -v /tmp/.X11-unix:/tmp/.X11-u Isabelle/DOF has two major pre-requisites: * **Isabelle:** Isabelle/DOF requires [Isabelle 2020](http://isabelle.in.tum.de/website-Isabelle2020-RC4/). - Please download the Isabelle 2019 distribution for your operating + Please download the Isabelle 2020 distribution for your operating system from the [Isabelle website](http://isabelle.in.tum.de/website-Isabelle2020-RC4/). * **LaTeX:** Isabelle/DOF requires a modern pdfTeX-engine supporting the \expanded{}-primitive. This is, for example, included in the [TeXLive 2019](https://www.tug.org/texlive/) (or later) diff --git a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy index 2cce6e57..c1bf0caa 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy @@ -51,7 +51,7 @@ subsubsection*[prerequisites::technical]\Pre-requisites\ text\ \isadof has to major pre-requisites: \<^item> \<^bold>\Isabelle\\bindex{Isabelle} (\isabellefullversion). - \isadof uses a two-part version system (e.g., 1.0.0/2019), + \isadof uses a two-part version system (e.g., 1.0.0/2020), where the first part is the version of \isadof (using semantic versioning) and the second part is the supported version of Isabelle. Thus, the same version of \isadof might be available for different versions of Isabelle. @@ -266,7 +266,7 @@ users are: \<^item> The file \inlinebash|ROOT|\index{ROOT}, which defines the Isabelle session. New theory files as well as new files required by the document generation (\eg, images, bibliography database using \BibTeX, local \LaTeX-styles) need to be registered in this file. For details of Isabelle's build system, please - consult the Isabelle System Manual~@{cite "wenzel:system-manual:2019"}. + consult the Isabelle System Manual~@{cite "wenzel:system-manual:2020"}. \<^item> The file \inlinebash|praemble.tex|\index{praemble.tex}, which allows users to add additional \LaTeX-packages or to add/modify \LaTeX-commands. \ @@ -552,7 +552,7 @@ figure*[figfig3::figure,relative_width="95",src="''figures/antiquotations-PIDE'' \ Standard antiquotations referring to theory elements.\ text\ The corresponding view in @{docitem_ref \figfig3\} shows core part of a document conformimg to the CENELEC 50128 ontology. The first sample shows standard Isabelle antiquotations -@{cite "wenzel:isabelle-isar:2019"} into formal entities of a theory. This way, the informal parts +@{cite "wenzel:isabelle-isar:2020"} into formal entities of a theory. This way, the informal parts of a document get ``formal content'' and become more robust under change.\ figure*[figfig5::figure, relative_width="95", src="''figures/srac-definition''"] diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index cb699e0e..17355032 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -220,22 +220,22 @@ text\ As ODL is an extension of Isabelle/HOL, document class definitions can therefore be arbitrarily mixed with standard HOL specification constructs. To make this manual self-contained, we present syntax and semantics of the specification constructs that are most likely relevant for the - developer of ontologies (for more details, see~@{cite "wenzel:isabelle-isar:2019"}. Our + developer of ontologies (for more details, see~@{cite "wenzel:isabelle-isar:2020"}. Our presentation is a simplification of the original sources following the needs of ontology developers in \isadof: \<^item> \name\:\index{name@\name\} with the syntactic category of \name\'s we refer to alpha-numerical identifiers - (called \short_id\'s in @{cite "wenzel:isabelle-isar:2019"}) and identifiers + (called \short_id\'s in @{cite "wenzel:isabelle-isar:2020"}) and identifiers in \inlineisar+" ... "+ which might contain certain ``quasi-letters'' such - as \inlineisar+_+, \inlineisar+-+, \inlineisar+.+ (see~@{cite "wenzel:isabelle-isar:2019"} for + as \inlineisar+_+, \inlineisar+-+, \inlineisar+.+ (see~@{cite "wenzel:isabelle-isar:2020"} for details). \<^item> \tyargs\:\index{tyargs@\tyargs\} \<^rail>\ typefree | ('(' (typefree * ',') ')')\ - \typefree\ denotes fixed type variable(\'a\, \'b\, ...) (see~@{cite "wenzel:isabelle-isar:2019"}) + \typefree\ denotes fixed type variable(\'a\, \'b\, ...) (see~@{cite "wenzel:isabelle-isar:2020"}) \<^item> \dt_name\:\index{dt\_npurdahame@\dt_name\} \<^rail>\ (tyargs?) name (mixfix?)\ The syntactic entity \name\ denotes an identifier, \mixfix\ denotes the usual - parenthesized mixfix notation (see @{cite "wenzel:isabelle-isar:2019"}). + parenthesized mixfix notation (see @{cite "wenzel:isabelle-isar:2020"}). The \name\'s referred here are type names such as \<^verbatim>\int\, \<^verbatim>\string\, \<^verbatim>\list\, \<^verbatim>\set\, etc. \<^item> \type_spec\:\index{type_spec@\type_spec\} \<^rail>\ (tyargs?) name\ @@ -256,13 +256,13 @@ text\ mathematical notations for $\lambda$-terms in Isabelle/HOL. Example expressions are: \inlineisar|1+2| (arithmetics), \inlineisar|[1,2,3]| (lists), \inlineisar|''ab c''| (strings), \inlineisar|{1,2,3}| (sets), \inlineisar|(1,2,3)| (tuples), - \inlineisar|\ x. P(x) \ Q x = C| (formulas). For details, see~@{cite "nipkow:whats:2019"}. + \inlineisar|\ x. P(x) \ Q x = C| (formulas). For details, see~@{cite "nipkow:whats:2020"}. \ text\ Advanced ontologies can, \eg, use recursive function definitions with - pattern-matching~@{cite "kraus:defining:2019"}, extensible record - pecifications~@{cite "wenzel:isabelle-isar:2019"}, and abstract type declarations. + pattern-matching~@{cite "kraus:defining:2020"}, extensible record + pecifications~@{cite "wenzel:isabelle-isar:2020"}, and abstract type declarations. \ text\Note that \isadof works internally with fully qualified names in order to avoid @@ -554,7 +554,7 @@ subsubsection\Experts: Defining New Top-Level Commands\ text\ Defining such new top-level commands requires some Isabelle knowledge as well as extending the dispatcher of the \LaTeX-backend. For the details of defining top-level - commands, we refer the reader to the Isar manual~@{cite "wenzel:isabelle-isar:2019"}. + commands, we refer the reader to the Isar manual~@{cite "wenzel:isabelle-isar:2020"}. Here, we only give a brief example how the \inlineisar|section*|-command is defined; we refer the reader to the source code of \isadof for details. diff --git a/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy b/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy index 29477734..f9037224 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy @@ -33,7 +33,7 @@ text\ \ text\ Semantic macros, as required by our document model, are called \<^emph>\document antiquotations\ - in the Isabelle literature~@{cite "wenzel:isabelle-isar:2019"}. While Isabelle's code-antiquotations + in the Isabelle literature~@{cite "wenzel:isabelle-isar:2020"}. While Isabelle's code-antiquotations are an old concept going back to Lisp and having found via SML and OCaml their ways into modern proof systems, special annotation syntax inside documentation comments have their roots in documentation generators such as Javadoc. Their use, however, as a mechanism to embed diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/root.bib b/examples/technical_report/Isabelle_DOF-Manual/document/root.bib index f69a462a..7b39616e 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/document/root.bib +++ b/examples/technical_report/Isabelle_DOF-Manual/document/root.bib @@ -17,10 +17,10 @@ year = 2019 } -@Manual{ wenzel:isabelle-isar:2019, +@Manual{ wenzel:isabelle-isar:2020, title = {The Isabelle/Isar Reference Manual}, author = {Makarius Wenzel}, - year = 2019, + year = 2020, note = {Part of the Isabelle distribution.} } @@ -41,7 +41,7 @@ ontological feedback during the editing of a document. In this paper, we give an in-depth presentation of the - design concepts of DOF{\^a}s Ontology Definition Language + design concepts of DOF's Ontology Definition Language (ODL) and key aspects of the technology of its implementation. Isabelle/DOF is the first ontology language supporting machine-checked links between the formal and @@ -321,18 +321,18 @@ year = 2019 } -@Misc{ kraus:defining:2019, +@Misc{ kraus:defining:2020, title = {Defining Recursive Functions in Isabelle/HOL}, author = {Alexander Kraus}, note = {\url{https://isabelle.in.tum.de/doc/functions.pdf}}, - year = 2019 + year = 2020 } -@Misc{ nipkow:whats:2019, +@Misc{ nipkow:whats:2020, title = {What's in Main}, author = {Tobias Nipkow}, note = {\url{https://isabelle.in.tum.de/doc/main.pdf}}, - year = 2019 + year = 2020 } @InProceedings{ wenzel:system:2014, @@ -455,10 +455,10 @@ year = 2019 } -@Booklet{ wenzel:system-manual:2019, +@Booklet{ wenzel:system-manual:2020, author = {Makarius Wenzel}, title = {The {Isabelle} System Manual}, - year = 2019, + year = 2020, note = {Part of the Isabelle distribution.} } diff --git a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy index f38b6b98..37acc0b1 100644 --- a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy +++ b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy @@ -21,7 +21,7 @@ open_monitor*[this::report] (*>*) title*[tit::title]\My Personal, Ecclectic Isabelle Programming Manual\ -subtitle*[stit::subtitle]\Version : Isabelle 2019\ +subtitle*[stit::subtitle]\Version : Isabelle 2020\ text*[bu::author, email = "''wolff@lri.fr''", affiliation = "\Université Paris-Saclay, LRI, France\"]\Burkhart Wolff\ diff --git a/src/ontologies/CENELEC_50128/DOF-CENELEC_50128.sty b/src/ontologies/CENELEC_50128/DOF-CENELEC_50128.sty index 80b58317..d5d07b72 100644 --- a/src/ontologies/CENELEC_50128/DOF-CENELEC_50128.sty +++ b/src/ontologies/CENELEC_50128/DOF-CENELEC_50128.sty @@ -14,7 +14,7 @@ \NeedsTeXFormat{LaTeX2e}\relax \ProvidesPackage{DOF-cenelec_50128} - [2019/08/18 Unreleased/Isabelle2019% + [2019/08/18 Unreleased/Isabelle2020% Document-Type Support Framework for Isabelle (CENELEC 50128).] \RequirePackage{DOF-COL} diff --git a/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty b/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty index 794dac6d..496981ef 100644 --- a/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty +++ b/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty @@ -14,7 +14,7 @@ \NeedsTeXFormat{LaTeX2e}\relax \ProvidesPackage{DOF-scholarly_paper} - [2020/01/14 Unreleased/Isabelle2019% + [2020/01/14 Unreleased/Isabelle2020% Document-Type Support Framework for Isabelle (LNCS).] \RequirePackage{DOF-COL} From 74ab956b11da0f472721e3a3d5a48d8ab3870e08 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Mon, 20 Apr 2020 18:51:04 +0100 Subject: [PATCH 6/7] Updated to the official Isabelle 2020 release and corresponding AFP version. --- .config | 6 +++--- install | 2 -- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/.config b/.config index d0c9a9f8..692faa9f 100644 --- a/.config +++ b/.config @@ -6,9 +6,9 @@ DOF_LATEST_DOI="10.5281/zenodo.3370483" DOF_GENERIC_DOI="10.5281/zenodo.3370482" # # Isabelle and AFP Configuration -ISABELLE_VERSION="Isabelle2020-RC4: April 2020" -ISABELLE_URL="https://isabelle.in.tum.de/website-Isabelle2020-RC4/" -AFP_DATE="afp-2020-04-17" +ISABELLE_VERSION="Isabelle2020: April 2020" +ISABELLE_URL="https://isabelle.in.tum.de/website-Isabelle2020/" +AFP_DATE="afp-2020-04-20" AFP_URL="https://www.isa-afp.org/release/"$AFP_DATE".tar.gz" # # Isabelle/DOF Repository Configuration diff --git a/install b/install index 4f1ff079..68d5b5ed 100755 --- a/install +++ b/install @@ -126,8 +126,6 @@ check_afp_entries() { fi done if [ "$missing" != "" ]; then - echo " Please install development version of AFP for Isabelle 2020 manually." - exit_error echo " Trying to install AFP (this might take a few *minutes*) ...." extract="" for e in $missing; do From aa74c32c7d1194109ea0d59e778a616d44a947e8 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Mon, 20 Apr 2020 18:54:22 +0100 Subject: [PATCH 7/7] Updated to the official Isabelle 2020 release and corresponding AFP version. --- README.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 96c2bbea..0446833a 100644 --- a/README.md +++ b/README.md @@ -20,9 +20,9 @@ foo@bar:~$ docker run -ti --rm -e DISPLAY=$DISPLAY -v /tmp/.X11-unix:/tmp/.X11-u Isabelle/DOF has two major pre-requisites: -* **Isabelle:** Isabelle/DOF requires [Isabelle 2020](http://isabelle.in.tum.de/website-Isabelle2020-RC4/). +* **Isabelle:** Isabelle/DOF requires [Isabelle 2020](http://isabelle.in.tum.de/website-Isabelle2020/). Please download the Isabelle 2020 distribution for your operating - system from the [Isabelle website](http://isabelle.in.tum.de/website-Isabelle2020-RC4/). + system from the [Isabelle website](http://isabelle.in.tum.de/website-Isabelle2020/). * **LaTeX:** Isabelle/DOF requires a modern pdfTeX-engine supporting the \expanded{}-primitive. This is, for example, included in the [TeXLive 2019](https://www.tug.org/texlive/) (or later) distribution. Please follow the [TeXLive installation instructions](https://www.tug.org/texlive/acquire-netinstall.html) @@ -41,7 +41,7 @@ one), the full path to the ``isabelle`` command needs to be passed as using the ``--isabelle`` command line argument of the ``install`` script: ```console -foo@bar:~$ ./install --isabelle /usr/local/Isabelle2020-RC4/bin/isabelle +foo@bar:~$ ./install --isabelle /usr/local/Isabelle2020/bin/isabelle ``` For further command line options of the installer, please use the