Introduction
This Eclipse plugin allows to edit files written in the Metamath language in the Eclipse IDE. It reuses the same core as MMJ2 and adds nice presentation.- Eclipse: http://www.eclipse.org/
- Metamath: http://us.metamath.org/
- MMJ2: http://wiki.planetmath.org/AsteroidMeta/mmj2/
Download
Here are links to the first versions of the Metamath Plugin for Eclipse:- 0.1.7.v20180417 - (LATEST)
- 0.1.6.v20170606
- 0.1.2.v20160710
- 0.1.0.v20110127
- 0.1.0.v20110122
- 0.1.0.v20110117
- 0.1.0.v20110114
It's still in the early stages, please report any issue you have with installing / bootstrapping.
Installation
The plugin is compatible with Eclipse Oxygen. [download]Currently, only the manual installation is possible: once the eclipse installation is finished, simply copy the emetamath plugin in the
eclipse/dropins
directory, or replace the previous version.I've had issues with the size of the
set.mm
file (it's almost 35Mb). I had to add the following lines to file eclipse/eclipse.ini
file:
-Xms256m -Xmx2048mSimply find the lines starting with "-Xms" and "-Xmx" and replace them with those values. They specify the heap size allocated to Eclipse.
First Use
The Metamath Perspective
The metamath perspective allows to have direct access to all features provided by the plugin (views are setup and opened, wizard shortcuts are displayed, etc.). In order to activate the perspective, from theWindow/Open Perspective/Others...
menu, choose Metamath
.
Creating a Metamath project
In order to create a new Metamath project, simply chooseFile/New/Metamath Project...
.You'll be prompted for a project name.
Adding files to the project
You can add files to your project using theFile/New/Metamath File...
menu.It is also possible to import an existing metamath file, ex. set.mm, either from the local system or from the metamath web site, by using the
File/Import...
menu, and selecting the respective Metamath File Import
choice.DONE: Fixed the long freeze times with
When loading the set.mm file itself, eclipse was hanging for a few seconds.
set.mm
. (cf. this article, eclipse bug 70412,etc.)When loading the set.mm file itself, eclipse was hanging for a few seconds.
Setting the main file
In order to be compiled, a your project needs to know with which file to start, i.e. which is the "main" file. Other .mm file may then be included from this one.You can set the "main" metamath file by choosing "set a main metamath file" from the contextual drop-down menu of the "Project Explorer" view.
The main metamath file is marked with a green triangle on the "Project Explorer" view.
TODO: Automatically tag the first metamath file added to a project as "main".
Features
The Project Explorer
The project explorer is a native eclipse view. The Metamath Plug-in enriches this view by marking the Metamath projects and files.Project Properties
The project properties page allow the user to change the main metamath file, and the base URL to use when displaying Metamath proof explorer web pages in the internal web browser.File Properties
The file properties allow to check whether a Metamath language file is currently the main metamath file or not.The Metamath Editor
The Metamath Editor is used for editing files with the extension".mm"
, written in the Metamath Language.
It provides syntax highlighting, details about the label when hovering, an intelligent selection method through double-click, and a contextual menu giving access to the following commands:
- Open Declaration - goes to the $c, $v or statement declaration for the selected metamath object
- Open Notation (for symbols only) - goes to the notation axiom for the selected metamath symbol, ex.
ctop
- Open Definition (for symbols only) - goes to the definition axiom for the selected metamath symbol, ex.
df-top
TODO: Enable "Open Notation" and "Open Definition" only when a metamath symbol is selected
TODO: Provide syntax highlighting also within comments, when correctly written ex. from
~ wtop
or ` J `
Hover information
When the mouse stays over a metamath element for a short time, a tool tip appears, giving more information about that element.DONE: Completed the information provided when hovering on a Metamath element: added element icon, name, hypothesis (for assertions), formula (for statements)
TODO: Also store the symbol's description when parsing Metamath language file, so that it can be displayed in the symbol's hover information
The Proof Assistant
To be completed.. (the buttons with "U" and "S" on the tool bar are the "unify" and "search unifiable assertions for this step" actions, respectively)The Step Unification Selection View
The Step Unification Selection view enables to select a unification to be applied on a given step of the Proof Assistant view.TODO: Enable the "Apply" action only when exactly one assertion is selected, or one of its children.
TODO: Allow the unification to take place also when clicking on the children nodes of a proposed unification.
TODO: Add other actions.
DONE: Corrected: When the proof worksheet was created from the "Open in Proof Assistant" action, and the proof worksheet is saved, the initial proof is used.
TODO: Correct: When the proof worksheet was created from the "Open in Proof Assistant" action, syntax highlighting is broken - has to do with line feeds.
The Proof Explorer View
The Proof Explorer view provides a quick way to locate or navigate through the metamath files. It shows the structure of the metamath project and its organization with chapters and sections.TODO: Shall I rename the view in order to avoid confusions with the web page also named "Metamath Proof Explorer"?
TODO: Add the scoping statements in the Proof Explorer view ?
TODO: Add an action to export the proof back to the origin MM file, optionally in compressed format.
TODO: Filter out hypotheses, and keep only theoremes and axioms
TODO: Display formulas instead of statement descriptions
The Proof Browser View
The proof browser view is similar to the Metamath "Proof Explorer" web page. For a given proof, it displays in tabular format, one proof step per line, and for each proof step its name, hypothesis, reference, and resulting expression.TODO: Also implement the "syntax breakdown" for axioms.
TODO: Also implement Chris Capel's "syntax breakdown" for axioms.
The Search View
TODO: Also search in the proof assistant worksheets ?
Project Properties
The project properties allow you to change the main metamath file in a project, the syntax coloring for the basic syntax types, and allows to enable/disable auto-transformations.The Metamath project properties can be accessed through the Project contextual menu in the project explorer, or from the Eclipse menu under 'Project'.
Preferences
The Metamath preferences allow you to set the proof formatting (text mode formula formatting/TMFF), and the bracket highlighting properties. Metamath preferences can be accessed through the overall preference menu.Source code
Source code can be found in GitHub.On the To-Do list
TODO: Add help pages.
TODO: Add proper properties pages.
TODO: Build a bundle with eclipse, set.mm, and emetamath plugin to allow a one-shot download and install.