Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity
2,072 Commits 14 Branches 9 Tags 76 MiB
Commit Graph

448 Commits

Author SHA1 Message Date
Makarius Wenzel 185daeb577 Tuned 2022-12-04 18:25:29 +01:00
Makarius Wenzel 8037fd15f2 Tuned messages, following isabelle.Export.message 2022-12-04 18:20:54 +01:00
Makarius Wenzel afcd78610b More concise export artifact 2022-12-04 18:03:53 +01:00
Makarius Wenzel b8a9ef5118 Tuned comments 2022-12-04 16:38:56 +01:00
Makarius Wenzel a4e75c8b12 Clarified export name for the sake of low-level errors 2022-12-04 16:35:55 +01:00
Makarius Wenzel d20e9ccd22 Proper session qualifier for theory imports (amending 44cae2e631)
ci/woodpecker/push/build Pipeline was successful Details
2022-12-04 00:45:07 +01:00
Makarius Wenzel f2ee5d3780 Tuned
ci/woodpecker/push/build Pipeline failed Details
2022-12-04 00:10:43 +01:00
Makarius Wenzel 44cae2e631 More formal management of ontologies in Isabelle/ML/Isar with output via Isabelle/Scala exports 2022-12-04 00:09:29 +01:00
Makarius Wenzel 7b2bf35353 More strict treatment of document export artifacts 2022-12-03 14:54:14 +01:00
Makarius Wenzel e8c7fa6018 Clarified signature 2022-12-03 14:44:04 +01:00
Makarius Wenzel b12e61511d Discourage etc/options
ci/woodpecker/push/build Pipeline was successful Details
2022-12-03 13:55:56 +01:00
Makarius Wenzel 3cac42e6cb Clarified order
ci/woodpecker/push/build Pipeline failed Details
2022-12-03 12:39:00 +01:00
Makarius Wenzel aee8ba1df1 Prefer DOF parameters over Isabelle options 2022-12-03 12:37:58 +01:00
Makarius Wenzel d93e1383d4 Afford full-scale command-line tool 2022-12-03 12:29:24 +01:00
Makarius Wenzel 96f4077c53 Tuned message
ci/woodpecker/push/build Pipeline was successful Details
2022-12-02 21:29:45 +01:00
Makarius Wenzel d7fb39d7eb Adhoc command-line tool replaces old options
ci/woodpecker/push/build Pipeline was successful Details
2022-12-02 21:14:55 +01:00
Makarius Wenzel 912d4bb49e Maintain document template in Isabelle/ML via Isar commands: 
result becomes export artifact, which is harvested by Isabelle/Scala build engine
 2022-12-02 20:05:15 +01:00
Makarius Wenzel a6c1a2baa4 Removed obsolete "extend" operation 2022-12-02 15:31:23 +01:00
Makarius Wenzel bb5963c6e2 Proper usage of dof_mkroot, although its Bash pretty-printing in LaTeX is a bit odd 2022-12-02 14:35:17 +01:00
Makarius Wenzel cc3e2a51a4 More antiquotations 2022-12-02 13:50:16 +01:00
Makarius Wenzel 9e4e5b49eb More antiquotations from Isabelle2021-1/2022 2022-12-02 11:41:31 +01:00
Makarius Wenzel b65ecbdbef Updated to Isabelle2022 2022-12-02 10:34:15 +01:00
Makarius Wenzel 3be2225dcf Tuned comments
ci/woodpecker/push/build Pipeline was successful Details
2022-12-01 22:54:01 +01:00
Makarius Wenzel f44f0af01c Use regular Toplevel.presentation from Isabelle2022, without alternative presentation hook 2022-12-01 22:48:45 +01:00
Makarius Wenzel 9a11baf840 Latex.output_name name is back in Isabelle2022 2022-12-01 22:04:56 +01:00
Makarius Wenzel 48c167aa23 Proper DOF.artifact_url 2022-12-01 21:45:06 +01:00
Makarius Wenzel 700a9bbfee clarified DOF.options: hard-wired document_comment_latex always uses LaTeX version of comment.sty 2022-12-01 21:30:32 +01:00
Makarius Wenzel 73299941ad Tuned 2022-12-01 17:26:29 +01:00
Makarius Wenzel 5a8c438c41 Omit excessive quotes 2022-12-01 16:48:33 +01:00
Makarius Wenzel 7772c73aaa More accurate defaults 2022-12-01 16:39:41 +01:00
Makarius Wenzel ca18453043 Clarified signature: more explicit types and operations 2022-12-01 16:28:44 +01:00
Makarius Wenzel 1a122b1a87 More robust default 2022-12-01 15:48:52 +01:00
Makarius Wenzel 47d95c467e Tuned whitespace 2022-12-01 15:33:16 +01:00
Makarius Wenzel bf3085d4c0 Clairifed defaults and command-line options 2022-12-01 15:26:48 +01:00
Makarius Wenzel 068e6e0411 Tuned 2022-12-01 14:23:00 +01:00
Makarius Wenzel 94ce3fdec2 Prefer constants in Scala, to make this independent from component context 2022-12-01 14:15:17 +01:00
Makarius Wenzel a6ab1e101e Update Isabelle + AFP URLs 2022-12-01 11:55:51 +01:00
Nicolas Méric 06833aa190 Upddate single argument handling for compute_attr_access
ci/woodpecker/push/build Pipeline was successful Details 
Trigger error when the attribute is not specified as an argument
of the antiquatation and is not an attribujte of the instance.
(In these case, the position of the attribute is NONE)
 2022-11-28 10:05:47 +01:00
Nicolas Méric 4f0c7e1e95 Fix type unification clash for trace_attribute term antiquotation
ci/woodpecker/push/build Pipeline was successful Details
2022-11-25 08:57:59 +01:00
Nicolas Méric 0040949cf8 Add trace-attribute term antiquotation
ci/woodpecker/push/build Pipeline was successful Details 
- Make doc_class type and constant used by regular expression
  in monitors ground
- Make class tag attribute ground (with serial())
- The previous items make possible
  the evaluation of the trace attribute
  and the definition of the trace-attribute term annotation
 2022-11-24 16:47:21 +01:00
Nicolas Méric e68c332912 Fix markup for some antiquotations
ci/woodpecker/push/build Pipeline was successful Details 
Fix markup for docitem_attribute and trace_attribute
ML and text antiquotations
 2022-11-24 11:22:02 +01:00
Burkhart Wolff b2c4f40161 Some LaTeX experiments with Achim
ci/woodpecker/push/build Pipeline was successful Details
2022-11-18 10:30:33 +01:00
Burkhart Wolff 309952e0ce syntactic rearrangements
ci/woodpecker/push/build Pipeline was successful Details
2022-11-09 11:19:00 +01:00
Burkhart Wolff 830e1b440a ported another Figure* in OutOfOrderPresntn to Isabelle2022
ci/woodpecker/push/build Pipeline was successful Details
2022-11-09 06:06:30 +01:00
Burkhart Wolff 2149db9efc semantics of fig_content (untested)
ci/woodpecker/push/build Pipeline was successful Details
2022-11-08 20:52:58 +01:00
Burkhart Wolff 1547ace64b added some semantics to fig_content
ci/woodpecker/push/build Pipeline was successful Details
2022-11-08 19:27:07 +01:00
Burkhart Wolff 29770b17ee added syntax for fig_content 2022-11-08 10:03:15 +01:00
Achim D. Brucker 873151b4f3 Update to Isabelle 2022.
ci/woodpecker/push/build Pipeline was successful Details
2022-10-30 17:56:15 +00:00
Achim D. Brucker cfdbd18bfa Resolved merge conflict. 2022-10-30 11:52:41 +00:00
Achim D. Brucker 0b807ea4bc Merge branch 'main' into Isabelle_dev
ci/woodpecker/push/build Pipeline failed Details
2022-10-30 11:22:13 +00:00
Makarius Wenzel 516f5d2f79 Merely use session structure instead of component settings. 2022-10-24 22:11:30 +02:00
Makarius Wenzel 5ac41a72ac More accurate treatment of sty files: do not just copy from all examples. 2022-10-24 21:58:10 +02:00
Makarius Wenzel 15feeb7d92 More standard package name: appears to work properly in Isabelle2022. 2022-10-24 21:38:01 +02:00
Makarius Wenzel 0c8a0e1d63 Adapted to Isabelle/1ac2416e8432 -- approx. Isabelle2022 release. 2022-10-24 21:30:49 +02:00
Burkhart Wolff 0aec98b95a cell row column parser setup
ci/woodpecker/push/build Pipeline was successful Details
2022-10-11 21:43:13 +02:00
Burkhart Wolff 43871ced48 text-term* and text-value* antiquotation syntax, and more on tables.
ci/woodpecker/push/build Pipeline was successful Details
2022-10-11 21:00:33 +02:00
Burkhart Wolff 0fa1048d6d description of the tab model.
ci/woodpecker/push/build Pipeline was successful Details
2022-10-10 13:51:54 +02:00
Burkhart Wolff 33490f8f15 table cell syntax implemented; roughly tested.
ci/woodpecker/push/build Pipeline was successful Details
2022-10-09 14:01:53 +02:00
Burkhart Wolff 01632b5251 hoisting cm pt syntax intp COL
ci/woodpecker/push/build Pipeline was successful Details
2022-10-06 16:59:42 +02:00
Burkhart Wolff 8a54831295 more elements for table parser.
ci/woodpecker/push/build Pipeline was successful Details
2022-10-03 08:23:05 +02:00
Burkhart Wolff 427226f593 some stuff with tables
ci/woodpecker/push/build Pipeline was successful Details
2022-09-27 12:16:31 +02:00
Achim D. Brucker 7f500dc257 Migration to latest Isabelle development version. 2022-08-11 23:04:07 +01:00
Achim D. Brucker 9f2e2b53a4 Merge branch 'main' into Isabelle_dev
ci/woodpecker/push/build Pipeline failed Details
2022-08-01 22:58:21 +01:00
Burkhart Wolff 583636404f renamed cenelec_document into cenelec_report.
ci/woodpecker/push/build Pipeline was successful Details
2022-08-01 21:50:49 +02:00
Burkhart Wolff 8a9684590a pass through miniôdo: deeper ontological reasoning, less LaTeX.
ci/woodpecker/push/build Pipeline was successful Details
2022-08-01 21:42:32 +02:00
Burkhart Wolff 81c4ae2c13 first version of new commands onto_class // doc_class
ci/woodpecker/push/build Pipeline was successful Details
2022-08-01 15:53:33 +02:00
Achim D. Brucker f40d33b9ed Ad-hoc port to development version of Isabelle.
ci/woodpecker/push/build Pipeline failed Details
2022-07-17 22:46:56 +01:00
Achim D. Brucker 6a94728747 Port to development version of Isabelle. 2022-07-17 20:47:17 +01:00
Burkhart Wolff c8a3c58f7f end of discussion with Achim
ci/woodpecker/push/build Pipeline was successful Details
2022-06-30 12:58:49 +02:00
Achim D. Brucker b24ede4400 LIPIcs needs to stay unsupported, right now. 2022-06-29 21:46:39 +01:00
Achim D. Brucker 205aa5a6b1 Moved core ACM styles into DOF-core.sty. 2022-06-29 21:45:09 +01:00
Achim D. Brucker c8f3bfc65d Removed unused imports. 2022-06-29 20:17:40 +01:00
Achim D. Brucker 44f9317b35 Integrated dof-common.tex into DOF-core.sty. 2022-06-29 20:12:32 +01:00
Achim D. Brucker 6c2a0d6876 Renaming to ensure compliance with naming restrictions.
ci/woodpecker/push/build Pipeline was successful Details
2022-06-29 19:08:56 +01:00
Achim D. Brucker 6c0d325673 Use full qualified name for templates.
ci/woodpecker/push/build Pipeline was successful Details
2022-06-26 19:06:49 +01:00
Achim D. Brucker b40069bedd Use full qualified name for templates. 2022-06-26 19:06:45 +01:00
Achim D. Brucker 9ded308371 Use full qualified name for scholarly_paper.
ci/woodpecker/push/build Pipeline was successful Details
2022-06-26 17:12:09 +01:00
Achim D. Brucker e6ca682114 Merge branch 'main' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF
ci/woodpecker/push/build Pipeline failed Details
2022-06-26 16:01:57 +01:00
Burkhart Wolff 013296f25e experiments on tables
ci/woodpecker/push/build Pipeline was successful Details
2022-06-26 13:48:03 +02:00
Achim D. Brucker 7c50ffb3af Refactoring. 2022-06-25 17:15:04 +01:00
Achim D. Brucker 3a9826901a Cleanup. 2022-06-25 17:11:01 +01:00
Achim D. Brucker a54373ad2f Merge branch 'config_as_options' 2022-06-25 16:36:46 +01:00
Achim D. Brucker a973707a73 Implemented -h. 2022-06-24 17:02:12 +01:00
Achim D. Brucker e138855623 Use comment.sty in LaTeX mode by default. 2022-06-24 16:07:25 +01:00
Achim D. Brucker 5278608b89 Merging main into config_as_options. 2022-06-24 15:57:59 +01:00
Achim D. Brucker 59658cea6f mkroot_DOF is not replaced by dof_mkroot, which is implemented in Scala. 2022-06-24 14:55:53 +01:00
Achim D. Brucker ef674b5ae2 Migrated, tested, and debugged new configuration setup. 2022-06-24 14:48:49 +01:00
Achim D. Brucker ac8c939179 Initial setup using configurations as options, retiring both the build script (LaTeX build) and the mkroo_DOF script (replaced by a Scala-based tooling). 2022-06-24 14:02:19 +01:00
Burkhart Wolff c16ec333f1 experiments on multi-commands - multi-figures
ci/woodpecker/push/build Pipeline was successful Details
2022-06-24 08:15:03 +02:00
Burkhart Wolff d1e4fd173b Experiments with multi-commands and -figures.
ci/woodpecker/push/build Pipeline was successful Details 
- added multi-arg syntax (only one arg evaluated so far)
- added figure_content built-in antiquotation
- added new Figure* - multi-arg command.
 2022-06-22 16:32:31 +02:00
Burkhart Wolff 43c857af2c roughly ported Latex testbench to 21-1
ci/woodpecker/push/build Pipeline was successful Details
2022-06-17 20:35:32 +02:00
Burkhart Wolff 0cc010cecc debugged merge
ci/woodpecker/push/build Pipeline was successful Details
2022-06-17 09:37:43 +02:00
Burkhart Wolff ba7bd6dc03 Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
ci/woodpecker/push/build Pipeline failed Details
2022-06-17 09:31:29 +02:00
Burkhart Wolff 43b0a3049f Modelling sample for tables 2022-06-17 09:31:17 +02:00
Nicolas Méric 03fd491d5d Implement CENELEC Table A.1
ci/woodpecker/push/build Pipeline was successful Details 
- Add an eager and lazy invariants checking functions mechanism
  for low level invariants to allow the checking of invariants
  only when opening or closing a monitor instance.
  The state of the monitor instances traces evolves when declaring
  instances between open_monitor* and close_monitor* commands.
  This mechanism can capture the changes be defining
  invariants before or after traces are populated but not
  before and after, with the current mechanism.
  Two tables were added: docclass_eager_inv_tab
  and docclass_lazy_inv_tab to store these invariants
- Implement CENELEC_50128 Table A.1 using this mechanism
 2022-06-13 07:56:53 +02:00
Nicolas Méric 9673359688 Enable high level invariants checking for some commands
ci/woodpecker/push/build Pipeline was successful Details 
Enable high level invariants checking for the update_instance*
and close_monitor* commands
 2022-05-27 17:14:17 +02:00
Nicolas Méric 5d1b271336 Allow access to the monitor table for low level invariants
ci/woodpecker/push/build Pipeline was successful Details 
When defining low level invariants checking functions,
access to the monitor table might be useful.
So the table should be populated before the checking takes place.
 2022-05-27 14:46:04 +02:00
Nicolas Méric 83c790d66a Handle normalization of trace attribute
ci/woodpecker/push/build Pipeline was successful Details
2022-05-26 12:56:21 +02:00
Nicolas Méric 9981c31966 Normalize docobj table value
ci/woodpecker/push/build Pipeline was successful Details 
Normalize the record registered as value in the docobj table,
i.e., the logical value of a docitem (a class instance)
 2022-05-25 17:10:57 +02:00
Nicolas Méric 319b39905f Update CENELEC_50128 implementation
ci/woodpecker/push/build Pipeline was successful Details 
- Update phase datatype to be accurate with 7.3 in the standard
- Update cenelec_document class: according to the table C.1 in the
  standard, written by, first check, and second check can be optional.
  See Phase Planning line 4 in the table, for example
- Some specifications are external to the standard: implement them
  as external_specification subclasses
- Fix phases attributes of classes
 2022-05-18 18:23:57 +02:00