Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity
1,579 Commits 15 Branches 10 Tags 77 MiB
Commit Graph

1579 Commits

Author SHA1 Message Date
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 909dda1ea2 Documented component registration. 2022-06-29 18:50:44 +01:00
Achim D. Brucker 367d8f28ad Improved installation instructions. 2022-06-29 16:25:32 +01:00
Achim D. Brucker d3f41dca9e In quick and dirty mode, do not require a clean build.
ci/woodpecker/push/build Pipeline was successful Details
2022-06-29 15:59:02 +01:00
Achim D. Brucker ae3d35e363 Fixed quick and dirty mode.
ci/woodpecker/push/build Pipeline was successful Details
2022-06-29 15:34:27 +01:00
Achim D. Brucker 41a6c22822 Optimised quick&dirty setup.
ci/woodpecker/push/build Pipeline was successful Details
2022-06-29 14:51:04 +01:00
Achim D. Brucker 4ac7c84403 Optimised quick&dirty setup.
ci/woodpecker/push/build Pipeline was successful Details
2022-06-29 13:57:07 +01:00
Achim D. Brucker 38f6516ad9 Optimised quick&dirty setup.
ci/woodpecker/push/build Pipeline was successful Details
2022-06-29 13:37:35 +01:00
Achim D. Brucker 03b721f014 Added renaming of mkroot_DOF.
ci/woodpecker/push/build Pipeline was successful Details
2022-06-27 06:40:18 +01:00
Achim D. Brucker c5752ba4a2 Grammar/spell-checking.
ci/woodpecker/push/build Pipeline was successful Details
2022-06-27 06:35:06 +01:00
Achim D. Brucker 5721398340 Documented document_build=dof option.
ci/woodpecker/push/build Pipeline was successful Details
2022-06-26 19:14:08 +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 70b2647e7c Using full-qualified names for ontologies in ROOT files. 2022-06-26 18:45:47 +01:00
Achim D. Brucker c1efddf252 Changed order of lualatex and pdflatex Ci build [CI SKIP]. 2022-06-26 17:23:53 +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 f63d922096 Fixed woodpecker config.
ci/woodpecker/push/build Pipeline failed Details
2022-06-26 16:56:46 +01:00
Achim D. Brucker 11b309da02 Only build distributin archive for lualatex build. 2022-06-26 16:46:56 +01:00
Achim D. Brucker 1444f8f48b Fixed outdated use of mkroot_DOF and added (not yet tested) setup to create build archive during CI build. 2022-06-26 16:35:23 +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
Achim D. Brucker 15fb6fdc2d Added quick-and-dirty mode. 2022-06-26 16:00:06 +01:00
Achim D. Brucker 9d5c71d4e1 Migrated release script to new setup using Isabelle options for configuration. 2022-06-26 15:24:49 +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 d10b277c60 Fixed documentation. 2022-06-25 17:34:08 +01: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 aa7d0aec09 Print help message, if script is invoked without prefixing 'isabelle env'. 2022-06-24 18:50:32 +01:00
Achim D. Brucker 31778374ed Read settings from options. 2022-06-24 18:45:48 +01:00
Achim D. Brucker 0d55da68de Removed unused option. 2022-06-24 17:49:04 +01:00
Achim D. Brucker a973707a73 Implemented -h. 2022-06-24 17:02:12 +01:00
Achim D. Brucker b83f7a8abb Updated manual. 2022-06-24 16:58:07 +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 5582644068 Improved description of latest changes. 2022-06-24 16:01:27 +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