Skip to content
This repository has been archived by the owner on Jun 26, 2023. It is now read-only.

Release notes

NormanPirk edited this page Dec 6, 2021 · 8 revisions

2nd iteration:

Deployment

Main View

  • On opening the application, a list of proofs is shown in the middle of the screen.
  • When any of the proofs are clicked, the user is directed to a detailed view of the clicked proof.
  • On the upper right side of the screen, there's a button "Create new proof" for creating a new proof.
  • On clicking the "Create new proof" button, the user is directed to a page for creating a new proof.

Proof View

  • When this view is opened, the proof's assumption and conclusion are presented.
  • Some proofs also contain a more detailed description of the problem and additional arguments.
  • Some arguments have additional details linked to it. The details can be seen by clicking on the corresponding argument. Then, the details can be closed by clicking on the argument.

Proof Creation View

  • A new proof can be fitted with an assumption, details, arguments and a conclusion. The corresponding text fields are shown in the middle of the screen.
  • On the lower left of the screen, there's a button "Create proof", which adds the proof to the list of proofs. WIP, may contain bugs
  • On clicking the "Create proof" button, the is directed to the detailed view of the newly-created proof.

Details of creating a new Proof

  • An assumption and a conclusion are must be filled before a new proof can be created.
  • A proof can be given a description by filling in the text box under 'Detailed'.
  • Arguments for the proof can be searched or chosen from the drop-down menu. Clicking the button "Add" will add the chosen argument to the list of proof's arguments and to the list of all arguments. WIP, may contain bugs
  • A new argument can be created for the proof. The argument requires a statement and can be given an optional detailed description. Clicking the button "Create" will add the chosen argument to the list of proof's arguments. WIP, may contain bugs

3rd iteration:

Deployment

New functionality

Signing in

  • On the main page there is a button for signing in. For signing in the user needs to first register using their GitHub account. After registration the users can sign in using sign in with GitHub.

Deleting theorems (proofs in the previous version)

  • If the user is signed in and has opened a proof, there is a button for deleting the proof. If the user is not signed in, the deleting option is not available.

Deleting proof sections when creating a new theorem

  • When a signed in user is creating a new proof, it is possible to add and remove proof steps by clicking on the + or - buttons next to the proof steps respectively.

Improvements

New structure for the theorem (proof in the previous version)

  • The proof was renamed to theorem
  • The theorem consists of a claim and proof steps.
  • Each proof step can have 0 or more substeps.

Theorem preview when creating a new proof

  • The preview of the theorem will be displayed below the section of theorem creation.

4th iteration:

Deployment

New functionality

Referencing from one step to another step or a subproof within a single theorem

  • When creating a theorem it is possible to reference from one step to another step or subproof. This can be done as follows:
    • Add a step you want to reference to. It gets automatically an order_nr before it.
    • Add a step or a subproof you want to reference from. In the statement field use ##order_nr## for referencing to the needed step.

Searching theorems

  • On the main page of the application there is a search field. Entering a search phrase goes through all the claims and steps and filters out the theorems that have a match.

Support for using LaTeX in theorems

  • When creating a theorem use:
    • for inline LaTeX - $ on both sides of the expression, for example: $\lambda$
    • for block LaTeX - $$ on both sides of the expression, for example: $$x^2=3y$$
  • Using spaces inside the LaTeX expressions does not work since the input will be split on spaces to find possible references to other steps.

Improvements and bug fixes

Navigating to main page from theorem creation or viewing pages

  • When creating or viewing a theorem there is a new button with a left arrow. Clicking on it directs you back to the main page.
  • If you were on the theorem creation page, the changes made there will not be saved.

A hint was added to the theorem creation page how to write expressions using LaTeX

Theorem creation only for authenticated users

Creating a theorem with empty steps

  • When trying to create a theorem with an empty step, the system asks to fill them in or delete them and will not let save the theorem.

When opening a theorem for viewing only clicking on the text opens the theorem

  • Now, when on main page, clicking on whenever on the theorem element opens the theorem for viewing.

Known bugs

LaTeX expressions that need whitespaces are not rendered correctly

  • In such cases there is a workaround which is to surround the symbol following the space with extra $-symbols. For example $\forall x$ -> $\forall$$x$.
  • An issue has been created for dealing with this: #66.

Functionality for future releases

  • Editing theorems UC-3
  • Referencing to a step in another theorem UC-8
  • Comment management UC-9, UC-10