日本語 (ja)

Compatible with DokuWiki

• 2024-02-06 "Kaos" yes
• 2023-04-04 "Jack Jackrum" unknown
• 2022-07-31 "Igor" unknown
• 2020-07-29 "Hogfather" unknown

• Download
• Report bugs

Provides dynamically verifiable documentation of mathematics using Mizar

Last updated on

2024-12-28

Provides

Syntax, Action

Repository

Source

Tagged with math, mizar, proof, theorem, verifier

By Yamada, M.

This plugin provides proof verification functionality using Mizar.

• Display blocks of Mizar articles side by side with regular content
• Syntax highlighting for Mizar code blocks
• Edit and compile Mizar code blocks in the view screen
• Display error messages and their locations
• Red wavy lines under error locations
• Tooltip error messages
• Local article references within the wiki using the miz2prel command
• Display and download the full article
• Copy Mizar code blocks to the clipboard

External requirements: This plugin requires the following additional components that must be installed separately:

• Mizar Downloads

Search and install the plugin using the Extension Manager. Refer to Plugins on how to install plugins manually.

See the plugin in action here. A more practical example of the page can be seen here.

Basic syntax:

<mizar your_article_name.miz>
  Write the Mizar article here.
  The article can be divided and written in compilable sections, 
  but the order must be maintained.
  It can be interspersed with regular content, including text, images, and diagrams,
  alongside the Mizar article.
</mizar>

• your_article_name must be the same throughout the page. A single page can contain only one article.

In the source view, the miz2prel button is displayed as follows. However, it is only visible during full edit mode and not in partial edit mode.

When the miz2prel button is pressed, the miz2prel command is executed on the article, formed by sequentially concatenating all sections enclosed by the opening and closing mizar tags from top to bottom, displaying the compilation result. The miz2prel button then changes to a Clear button. If there are any errors, the error locations and corresponding error messages are displayed. If the compilation is successful, the article becomes accessible for local reference within this wiki.

When the Clear button is pressed, the compilation result display is cleared, and the files in the TEXT subdirectory of the Mizar working directory is deleted.

The rendered result is as follows: each section enclosed by the mizar tag is displayed as a syntax-highlighted code block format (see also here) with cumulative line numbering, a file name, a Copy button, and an Edit button.

When the file name is clicked, the article—formed by sequentially concatenating all blocks from top to bottom—is displayed as shown below and can also be downloaded as a .miz file.

When the Copy button is pressed, the contents of the article block are copied to the clipboard.

When the Edit button for a block is pressed, it changes to a Reset button and a Compile button, as follows.

At this time, the article block changes from read-only to editable. Note that this occurs directly on the View screen, not in the source view, allowing anyone to edit regardless of user permissions. However, this does not alter the source article itself. To modify the source article in the source view, edit permissions are required. The line numbers in each article block are synchronized with this edit, allowing all of them to be treated as a single article.

When the Reset button is pressed here, the content of that block reverts to the original source block content, and the buttons also return to their initial state.

When the Compile button on a article block is pressed, the makenv and verifier commands are executed on a .miz file created by sequentially merging all blocks up to that block, displaying the compilation result below the article block. If there are any errors, links to the error locations and corresponding error messages are shown below the article block. Additionally, red wavy lines appear under the error locations. Hovering over these underlined sections displays the error message as follows.

When the Reset button on a article block is pressed, the compilation result display for that article block is cleared, the content of the article block reverts to the original source block content, and any red wavy underlines are removed. Additionally, the files in the TEXT subdirectory of the Mizar working directory are deleted, and the buttons also return to their initial state.

Click the Admin button on your page, then select Configuration Settings from the Administration Menu. In the Plugin section, find Mizar verifiable docs and enter the following items:

• Mizar work directory (includes subdirectories like TEXT, DICT, and PREL)
• Mizar shared files directory
• Mizar executables directory

On Windows platforms, the Mizar shared files directory and the Mizar executables directory are the same, e.g., c:\mizar; see also the ReadMe for Windows. On Linux, the default Mizar shared files directory is /usr/local/share/mizar, and the Mizar executables directory is /usr/local/bin. See also the README for Linux.

The source code of the plugin is available at GitHub: https://github.com/YamadaMiz/mizarverifiabledocs.

• The Hide/Show button allows you to collapse and expand the editor and… (2024-12-28 03:45)
• Enhance folding functionality with `proof ... end` support, (2024-12-22 09:41)
• Add article display in new tab with .miz file download option (2024-11-30 09:27)
• Modify plugin.info.txt (2024-11-30 04:51)
• Add filename validation and update syntax to omit file extension (2024-11-30 04:30)
• Renamed the plugin from "Mizar Proof Checker" to "Mizar Verifiable Docs" (2024-11-28 11:51)
• button name: mizf to Compile (2024-11-23 09:09)
• Create README.md (2024-11-21 04:13)

GitHub Issues

[developers roadmap]

[discussions should ideally be deleted and turned into FAQ entries along the way]