日本語 (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

2025-03-29

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

In this article, we explain the Linux version. Please refer to the README for Linux (i386) available on the Mizar Downloads page.

If your Linux server is running in a 64-bit environment, but you need to use the Linux (i386) (32-bit) version, then you must install 32-bit compatibility libraries.

sudo dpkg --add-architecture i386
sudo apt-get update
sudo apt-get install libc6:i386 libstdc++6:i386

Download and extract the 32-bit version of Mizar. Make sure to update this to the latest version available at:

https://mizar.uwb.edu.pl/~softadm/pub/system/i386-linux/

cd /usr/local/src
wget https://mizar.uwb.edu.pl/~softadm/pub/system/i386-linux/mizar-8.1.14_5.84.1473-i386-linux.tar 
tar -xvf  mizar-8.1.14_5.84.1473-i386-linux.tar 

Run the installation script using the following command:

sudo ./install.sh --default

Setting the MIZFILES Environment Variable

echo 'export MIZFILES=/usr/local/share/mizar' >> ~/.bashrc
source ~/.bashrc

Checking if /usr/local/bin is in your PATH

echo $PATH

Extracting the Executables

cd /usr/local/bin
tar -xvzf /usr/local/src/mizbin.tar.gz -C /usr/local/bin

To set up Mizar, create a dedicated working directory in the document root of your web server (e.g., Apache or Nginx). Within that folder, create three subdirectories: DICT, prel, and TEXT.

For example, if your document root is /var/www/html, you can run the following command:

mkdir -p /var/www/html/mizarwork/{DICT,prel,TEXT}

Permission settings

• Ensure that the plugin directory is owned by www-data to allow uninstallation via DokuWiki's Extension Manager.
• Use minimal permissions so that only the owner (www-data) has full access.

chown -R www-data:www-data /var/www/html/dokuwiki/lib/plugins/
chown -R www-data:www-data /var/www/html/mizarwork
chmod -R 700 /var/www/html/mizarwork

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

In DokuWiki, navigate to Management → Site Settings → Installed Plugins: Plugin: Mizarverifiabledocs and enter the following settings:

• Mizar Working Directory (including subdirectories TEXT, DICT, PREL):
• Mizar Shared Files Directory:
• Mizar Executable Directory:

If your directory structure matches the one described in the above, the default settings will be sufficient.

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

Basic syntax:

<mizar your_article_name>
  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.

Note: In the following figure (GIF animation), the Mizar start tag (article name) includes the .miz extension. In the current version, the .miz extension is not required. Please specify only the article name without the extension.

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.

• Set MIZFILES environment variable in PHP to fix "mml.ini not found" e… (2025-03-29 09:40)
• Fix indentation logic for Proof and related nodes (2025-01-22 08:03)
• Add numbering to each editor on the page (2025-01-15 13:30)
• Add code folding support for DefinitionBlock, NowBlock, and HerebyBlock (2025-01-12 04:49)
• Add "Reset All" button for resetting all Mizar editors (2025-01-10 09:30)
• Add "Hide All" button to toggle visibility of all Mizar blocks (2025-01-04 09:44)
• 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)

GitHub Issues

[developers roadmap]

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