Yamma

[Antony Bartlett]

Glauco wrote:

> Antony wrote:

>>I'm still hoping I can figure out how to use Glauco's parser, but I realise I've been frittering away my spare time writing docker containers full of metamath command line tools, and working through David A Wheeler's video in mmj2 and yamma as Glauco recommended, instead.  However, I do intend to be back on the parse issue that's perhaps become a bit of a blocker for both of us, soon.  

> Hi Antony, feel free to open issues in the yamma repository, I'll be more than happy to help you to try a "Run Client" session :-)

I've got it working, thanks :-)

mmj2's great, I really like the unifier.  As a text editor... well I'm thrilled you're porting the core functionality to Visual Studio Code (VSC) - an integrated development environment that I, and probably literally millions of other developers use every work day (74% of respondents in the 2022 StackOverflow developers survey use it).  I think you've underplayed the significance of your project Yamma, and it's going to become a major factor in metamath's near future ("near" from the perspective of a project that started in 1992, at any rate).  Of course to capture the biggest audience for metamath we would also want tools to run in people's browsers including on their mobile phones, and the fact you're targeting the JavaScript platform is also a good step in that direction (even while it's more Samuel and I that have our eyes on that target).

Glauco wrote:

> it's clearly not yet ready for prime time

The biggest obstacle to me following David's video in yamma is that the LOC_AFTER feature of a .mmp file doesn't seem to be working yet.  So it keeps trying to unify and prove reccot from reccot, which is cute and amusing but not very practical.  I assume you would have fixed this by now if it was easy, so I plan to work around it with a simple command line tool for truncating a .mm file once I am comfortable with your parser.  I realise that's become something of a mantra for me, there are at least four things I plan on doing once I am comfortable with your parser.  Fortunately I will have run out of displacement activities once I hit 'send' on this email ;-)  Generating a .mmp file from a .mm file is another possible task for me once I am properly armed with a parser.  (getting a working demo of it streaming is the only item not relevant to the present discussion).

Finally, one smaller matter, I notice your unifier puts long terms on a single line (unlike mmj2), and suggest the best way for us npm users to sort that out is with a prettier plugin.  I've already got one for .mm files:

https://github.com/Antony74/prettier-plugin-mm

It's based off of the checkmm verifier which I haven't bothered to switch off.  As such it will on prettify verifiable .mm files, whereas ideally we want it to prettify any parsable .mm or .mmp file.  I'm planning to do the relevant rewrite "once I am comfortable with your parser" ;-)

Hope the feedback I've given is helpful (even though I don't seem to be able to shut up about parsers).

    Best regards,

        Antony

[Glauco]

I've got it working, thanks :-)

This is cool! (I've never even tried it myself, to clone the repository in a new folder)
Unfortunately, I still feel I'm a newbie about the npm / package.json / tsconfig.json / launch.json architecture, so your support is really welcome.

Please, let me know if / how I could rewrite the installation instructions so that a TS developer would be able to "compile" the "project" :-)

 

The biggest obstacle to me following David's video in yamma is that the LOC_AFTER feature of a .mmp file doesn't seem to be working yet.  So it keeps trying to unify and prove reccot from reccot, which is cute and amusing but not very practical.  I assume you would have fixed this by now if it was easy

I've never been able to make LOC_AFTER to work in mmj2 (but for years I've been using a "custom" version, that Mel wrote / maintained for a limited period of time; does LOC_AFTER work in your mmj2 installation?).
I've simplified (I believe) the header structure of .mmp files:
Yamma expects a
$theorem <label>
as a first statement (in the next few days, I plan to feat code to add this line automatically when a ctrl+u is performed; it needs to match the .mmp file name, otherwise a diagnostic / quickFix is displayed)
Now, it is used to check that your theorem is consistent with the database version (if you are refactoring an already existing theorem).
And it will be used to check that the eHyps labels are coherent (<label>.xxx format), otherwise a warning / quickFix is risen (the quickFix can be to either change the label or to add a statement $allowanyhyplabel , that suppresses this kind of warning, for this .mmp file)

Since there's interest, I will add a new statement
$locateafter <label>
(it shouldn't be hard to implement; but it has to be handled both in StepDerivation, in Search statements, and in StepSuggestions)

If you've not tried a Search yet, you can simply invoke it with ctrl + h (same as in mmj2); yamma will analyze the statement under the cursor and populate the search with the most "relevant" symbols (the 3 least frequent ones, if I remember correctly). The "Search Comment:" part is not implemented, yet. And a semantic tokenization for the keywords, is deserved... (near to the top of my current TODO list)

 

Generating a .mmp file from a .mm file is another possible task for me once I am properly armed with a parser.

Absolutely (the same as ctrl+g in mmj2). Thierry already had this feature with its rust language server, metamath-vspa
https://github.com/tirix/metamath-vspa
(Thierry has written a number of impressive theorems and tools!)
This feature is really important, I use it a lot with mmj2, both to refactor proofs for existing theorems, and to write proofs for new, but "similar", theorems.
But I was planning to leave this feature for the second release of yamma (I'm still working on the first one...)
The other "popular" feature that I was planning to leave for the second release, is "renumbering" ( alt + u + r in mmj2)
I understand one expects these features to be there, but I cannot keep adding stuff, otherwise I will never be able to publish something for metamathicians to play with (and give some feedback)

 

Finally, one smaller matter, I notice your unifier puts long terms on a single line (unlike mmj2)

If I'm not mistaken, mmj2 has two/three modes
1. all statements in single line
2. all statements in multiple lines (with standard formatting)
3. "some" statements in multiple lines (with standard formatting)

You can toggle between 1. and 2. using ctrl + o
I'm always in mode 1. (single line) and then, selectively, reformat the single statement I'm focusing on (with right click > "Reformat Step: Swap Alt" ; sometimes, you have to do it twice, to actually work)

Of course, the plan is to port these 3 modes to yamma, too (only mode 1. is available, now)

But now I see what you mean: if you break a statement on multiple lines "by hand", mmj2 keeps your formatting, after a unification. In mmj2 I'm constantly typing ctrl + r to get the "standard" formatting, thus my custom formatting would not survive for long :-)
(as a side note, yamma ctrl+u triggers the "DocumentFormatting" language server protocol standard request, I guess that in my mind it's always been derive/unify/reformat)

Thanks again for having found the time to play with yamma, your feedback is really precious!

Glauco

[David A. Wheeler]

Weird, I never had a problem with LOC_AFTER in mmj2.

A quick workaround in another prover is, if you're trying to prove something,
don't reuse its proof in the database - instead stop reading at that point.
After all, if you're trying to prove "foo", then reusing "foo" seems counterproductive :-).

--- David A. Wheeler

> --
> You received this message because you are subscribed to the Google Groups "Metamath" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/70437437-193e-43ab-b576-9ea758811267n%40googlegroups.com.

[Antony Bartlett]

Just for the sake of clarity:

1.

David wrote:

>Glauco wrote:

>> I've never been able to make LOC_AFTER to work in mmj2 (but for years I've been using a "custom" version, that Mel wrote / maintained for a limited period of time; does LOC_AFTER work in your mmj2 installation?).

>

>Weird, I never had a problem with LOC_AFTER in mmj2

Yes I'm afraid, Glauco, that LOC_AFTER works fine in mmj2 for me too.

2.

Glauco wrote:

> Please, let me know if / how I could rewrite the installation instructions so that a TS developer would be able to "compile" the "project" :-)

Cool, I've got a pull request in with some getting started instructions.  They're just suggestions, don't take any documentation unless you want it (or take it then rearrange to suit you).

https://github.com/glacode/yamma/pull/1

    Best regards,

        Antony

[Glauco]

Cool, I've got a pull request in with some getting started instructions.  They're just suggestions, don't take any documentation unless you want it (or take it then rearrange to suit you).

https://github.com/glacode/yamma/pull/1

Merged, thank you!

Have you tried it in Windows, or Linux?  (I've written yamma in Ubuntu 2016.4 and Ubuntu 2020.4, I've not tried it in Windows, yet)

I'll have to use your instructions myself...   :-)

Glauco

[Antony Bartlett]

On Sun, Dec 25, 2022 at 7:07 PM Glauco <glaform...@gmail.com> wrote:

Have you tried it in Windows, or Linux?  (I've written yamma in Ubuntu 2016.4 and Ubuntu 2020.4, I've not tried it in Windows, yet)

I've tried it on Windows.  As I also use a MacBook for work, I've got a reasonable sense of the differences between shell and command prompt, and the almost exactly-the-sameness of Visual Studio Code on either platform.  As such, I believe the instructions I've given are cross-platform.  However, if developers do run into difficulties running Yamma, I'm afraid they'll just have to let us know,

    Best regards,

        Antony

[Glauco]

I saw your screenshots for the configuration, and it was clear you did those on a c:\... hard drive ; sorry for having asked an obvious question.

Glauco

[Antony Bartlett]

On Sun, Dec 25, 2022 at 8:34 PM Glauco <glaform...@gmail.com> wrote:

I saw your screenshots for the configuration, and it was clear you did those on a c:\... hard drive ; sorry for having asked an obvious question.

Lol, nice deduction, no worries.

Also it was Christmas Day, we were lucky to find each other sober! ;-)

    Best regards,

        Antony

[Thierry Arnoux]

Hi Glauco,

I have again been away from Metamath for some time, but I see you have
persevered in the development of Yamma. How far are you?
Can now I simply install and use the VSCode extension from the VSCode
Marketplace?

Thanks,
_
Thierry

[Glauco]

Hi Thierry,

You can absolutely try it. I'm now using it in place of mmj2.

I'm using it in linux VMs, but I expect it to work on Windows, too. I don't have a Windows machine with node.js installed, to try it out.

If you have node.js installed, you should simply install it from the VS Code marketplace (I hope; with linux it worked out of the box).

You open a .mmp , and it activates the extension (it takes a few seconds to parse the main .mm file, see the progress notification on the bottom left)

It works better with an additional .mms file, that's a model for "step suggestions" (I'll explain it to the group, when I can).
At present, set.mms is a 33 MB text file. You can create it, launching the script
/yamma/server/src/stepSuggestion/ModelBuilderScript.ts
it takes a couple of hours in my VM. I could probably make it dramatically faster, building parsing trees directly from proofs, rather than running the early parser on every formula of every step of every proof.
If someone has a "place" to publish the model, I will send the set.mms.zip file (5Mb size), so everybody can download it.
I should add a command to launch the model builder from within Yamma.

Full "step derivation" is available a couple of minutes after the .mm is parsed (it is single step, but imho it is really powerful: it infers any kind of statement I've tried, in any proof: even with ten or more parameters, and in long proofs).

I hope you'll try it.

(DISCLAIMER: while writing formulas, now and then, there's some slowdown because the language server is sending a superlong error diagnostic for every character you type: I will leave this as a "verbose" non default option, but a shorter diagnostic message should fix it)

Please, let me know how it goes.

Glauco

[Thierry Arnoux]

Hi Glauco,

That's excellent news!

I had a quick try and saw some error messages. We can track that in the GitHub project issues from here on.
I'm excited to get Yamma to work!

BR,
_
Thierry

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/7e2db0cb-d8c8-42f6-b3a8-387d13a7127an%40googlegroups.com.

[Glauco]

Hi Thierry,

sure, post issues in the Repo.

Glauco

[Glauco]

26 april 2023  20:58:45 UTC+2 Glauco wrote:

(DISCLAIMER: while writing formulas, now and then, there's some slowdown because the language server is sending a superlong error diagnostic for every character you type: I will leave this as a "verbose" non default option, but a shorter diagnostic message should fix it)

I've just published ver.0.0.4 that has a new configuration parameter for the diagnostic message, for theory's formula syntax errors:

  - "short" (default) does not slow down typing

  - "verbose" gives full details about the expected characters and why the theory grammar requires them  (for large grammars, it could slow down typing, since the diagnostic is sent for every character)

Glauco

 

[Glauco]

version 0.0.7 has been published. It supports a

$getproof <label>

statement. This new feature serves as a counterpart to the mmj2 Ctrl+G functionality, allowing you to retrieve specific proofs effortlessly.

A number of bugs have been fixed. Special thanks to @tirix for his precious feedback and contributing to the bug reports.

[Glauco]

Version 0.0.10 has been published: you can now create a model for step suggestions directly within the extension, eliminating the need for external scripts.

The usual VSCode progress notification will keep you informed throughout the process, which typically takes about an hour on a slow VM.

(To create the model, open an .mmp file, and then press Ctrl+Shift+P and type "Create Model" or right-click and select "Create Model.")

[Glauco]

Yamma 0.0.11 Released (for easier theorem refactoring)

Yamma now builds a (partial) theory, even if some proofs are not valid.

This is a feature that I wish mmj2 had, because it allows for easier change of theorems' signatures.

Here's an example of how it works: in set.mm, ~ liminfgelimsupuz was written for sequences of reals. It had this (3rd) hyp

|- ( ph -> F : Z --> RR )

But it was easy to amend its proof for extended reals. So you can go in set.mm and change its third hyp to

|- ( ph -> F : Z --> RR* )

When Yamma reloads set.mm it will of course create Diagnostics for validation errors, and it will send you a final warning notification (for the whole theory being invalid).

But it will load all the valid theorems, anyway (a valid subtheory)

These are the Diagnostic errors you will get

Theorem liminfgelimsupuz : $e hypothesis doesn't match stack entry. The current hypothesis on the stack is '|- ( ph -> F : Z --> RR* ) . The $e hyp with substitution is |- ( ph -> F : Z --> RR ) .
Theorem climliminflimsup2 : Provable statement liminfgelimsupuz is in the theory, but its verification failed
Theorem climliminflimsup3 : Provable statement liminfgelimsupuz is in the theory, but its verification failed
Theorem climliminflimsup4 : Provable statement climliminflimsup2 is in the theory, but its verification failed
Theorem climliminflimsup4 : Provable statement liminfgelimsupuz is in the theory, but its verification failed
Theorem xlimliminflimsup : Provable statement climliminflimsup3 is in the theory, but its verification failed

You see that you need to fix the proof of liminfgelimsupuz, and then the "immediately" dependent proofs of climliminflimsup2 , climliminflimsup3 and  climliminflimsup4.

xlimliminflimsup is fine because it does not depend immediately on liminfgelimsupuz, thus it does not need any change

Now you can open the liminfgelimsupuz.mmp file and fix its proof, and create the .mmt file.
Then use climliminflimsup2.mmp and climliminflimsup3.mmp to fix their proofs.
Finally, use climliminflimsup4.mmp to fix its proof.

The whole theory will then be valid.

BR
Glauco

[Jim Kingdon]

On November 26, 2023 6:41:32 AM PST, Glauco <glaform...@gmail.com> wrote:
>Yamma now builds a (partial) theory, even if some proofs are not valid.

Ooh nice. I have my workarounds to handle these kinds of changes using mmj2 but having the tool understand it better sounds like it could be a significant help.

[Glauco]

My workaround with mmj2 was (given ~ example to be changed):

- create a ~ exampleNEW (with the new signature)

- search all proofs using ~ example

- load each in mmj2 and change it to use ~ exampleNEW  (then create the .mmt files)

- remove ~ example from the theory and reload the theory

- copy ~ exampleNEW and rename it to ~ example

- load in mmj2 each proof using ~ exampleNEW and change it to use the new ~ example

- remove ~ exampleNEW

I'd like to know if there is a better workflow in mmj2

[Jim Kingdon]

Not that I'm discouraging you from making this better in Yamma but what I do in mmj2 is:

1. Load the file in mmj2 and save .mmp files for everything I want to work on. Quit mmj2.

2. Go to a text editor and make changes to hypotheses or whatever it is.

3. Load the .mmp files. Steps that don't work any more will show an error but you can use mmj2 to help fix those errors (there's a bit of an art to that given how mmj2 handles different kinds of errors but I won't attempt to describe that in full detail here).

What you describe for mmj2 also works, I'm pretty sure I sometimes do that too (for some changes having the old and new both around at the same time can be helpful).

[Glauco]

Yamma 0.0.12 Released:

* Completion items in step suggestions now are not duplicated (when coming from multiple classifiers) and sorted by the Wilson Score (left bound of the 95% confidence interval)

* Removed erroneous empty line in compressed proof formatting (when the parenthesis closing the labels was the last character on its own line)

* Fixed issue with transformation being applied to hypotheses of existing theorems

[Glauco]

Yamma 0.0.15 Released:

* improved error notification and diagnostics when loading .mmt files

* $getproof now also loads $d statements for the specified theorem

* the theory multiple load problem has been fixed. ([#14](https://github.com/glacode/yamma/issues/14))

* minor bug fixes (for instance, ([#15](https://github.com/glacode/yamma/issues/15)) )

[Glauco]

Yamma 0.0.16 Released:

### Version 0.0.16 (2025-01-01)

#### Added  

- **New Command**: "Remove unused statements" – Cleans up unused statements in a proof, making it easier to finalize. This command can also be used during proof construction, even if the proof is incomplete.  

#### Improved  

- **ProofStepDuplicateRemover**: Enhanced handling of duplicate proof steps, including those with labels.  
  - Duplicate steps are now removed unless:  
    1. The step is proven.  
    2. The preceding step with the same formula is unproven.  

#### Fixed  

- **.mm and .mmt Parsing**: Replaced residual `throw error` statements with `DiagnosticError`, preventing crashes and improving error reporting.  

- **Caching of Formulas with Working Variables**:  
  - Excluded formulas containing working variables from the cache to prevent invalid cache usage.  
  - This addresses issues caused by the unification algorithm modifying these formulas during operations.  


The recent fix for formula caching addressed a potential issue that could cause unexpected behavior when switching tabs between two or more proofs.

I encourage yamma users to update to the latest release to benefit from this fix and other improvements

Glauco

[Glauco]

I forgot to mention that currently, the set.mm maintainers are actively renaming many well-known labels (e.g., ffvelrn has been renamed to ffvelcdm). To ensure that Yamma provides better suggestions, I recommend running the "Create Model" command. This step will be less critical once the relabeling project is complete, but for now, it can significantly enhance Yamma's accuracy.  

[Jim Kingdon]

On January 1, 2025 11:46:50 AM PST, Glauco <glaform...@gmail.com> wrote:
>
>
> This step will be less critical once
>the relabeling project is complete, but for now, it can significantly
>enhance Yamma's accuracy.

There has been some kind of renaming going on the whole time I've worked on set.mm but I guess you are right that some of the recent ones have involved some particularly widely used theorems.

This is not likely to end soon, see changes-set.txt in the set.mm repository for a list of proposed renames (which includes some very widely used theorems including syl)

[Glauco]

Yamma 0.0.17 Released:

Management of Discouraged Theorems: New features have been added to help users handle discouraged theorems more effectively.

Enhanced Step Suggestions: Step suggestions are now fully filtered on the server side, ensuring that VSCode does not apply additional filtering. This resolves the issue where useful label suggestions were being inadvertently excluded by VSCode, making them visible to users again.

### Version 0.0.17 (2025-01-25)

#### Added

• A new diagnostic warning is added when a .mmp proof step is justified using a label that refers to a statement with a 'new usage is discouraged' tag.
• Introduced the `$allowdiscouraged` directive in .mmp proofs.
  • Proofs containing this directive will bypass warnings when using labels tagged with 'new usage is discouraged.'
  • Proofs with the `$allowdiscouraged` directive will be generated if they are complete.
• The new diagnostic warning contains a 'Quick Fix' that automatically adds the $allowdiscouraged directive

#### Changed

Proofs that use labels tagged as 'new usage is discouraged' are no longer generated, even if complete, unless the `$allowdiscouraged` flag is present.


#### Improved
CompletionItems for step suggestions are now completely filtered on the server and additional client side filtering is disabled (previously, useful label suggestions were filtered out by VSCode, and not shown to the user)

[Glauco]

### Version 0.0.18 (2025-02-09)

#### Added
- **Support for unproven statements and warnings in `MmParser`**  
  - Introduced `MmParserWarningCode.unprovenStatement` to detect unproven statements (`$= ? $`).
  - Added the `containsUnprovenStatements` flag in `MmParser` to track theories with unproven statements.
  - Implemented `addDiagnosticWarning` to emit warnings for unproven statements during parsing.
  - Updated `TheoryLoader` to notify users when a theory contains unproven statements.

- **Support for the file inclusion command (Metamath Book, Section 4.1.2: 'Preprocessing')**  
  - Multiple `include` statements are supported, but each must be written on a single line (i.e., it cannot span multiple lines).  
  - Recursive file inclusion is supported.  
  - `.mm` tokens now retain information about the `.mm` file they originate from.  
  - Diagnostic errors and warnings are reported for each specific `.mm` file.  



This update was developed to address the following issues and PRs:  
- [Issue #17](https://github.com/glacode/yamma/issues/17)  
- [Issue #18](https://github.com/glacode/yamma/issues/18)  
- [PR #4578](https://github.com/metamath/set.mm/pull/4578)  

I’ve added a number of unit tests to ensure these features work as intended. However, since I don’t use these features extensively myself, your feedback is important. If you notice anything that doesn’t work as expected, feel free to open an issue on the [Yamma GitHub repository](https://github.com/glacode/yamma).

[Glauco]

As a side note, VSCode has a couple of handy features that might be useful for Metamath users:

1. **Yamma and the Problems Tab**  
   When using Yamma, it might be helpful to keep the **Problems tab** open. By default, the tab shows all warnings and errors across your entire workspace, which can be useful if you’re working with multiple `.mmp`, `.mm`, or `.mmt` files. Files with issues are also highlighted in the left navigation bar with small numbers, making it easy to identify "problematic" files.  

   However, if you want to focus on a single file, you can enable the **"Show active file only"** filter in the Problems tab. This will display only the diagnostics for the `.mmp` file you’re currently working on, which is ideal when you’re deep into a proof and want to avoid distractions.

2. **GitHub Copilot Integration**  
   If you’re using **GitHub Copilot** (which is kind of free for GitHub users—likely all of us here), you can enable it in your workspace. It works seamlessly alongside Yamma and provides continuous, non-intrusive suggestions. While the suggestions are not so good yet, they’re improving over time. The more proofs Copilot sees, the better it should become at assisting with Metamath-related tasks.

Have fun!
Glauco

[Thierry Arnoux]

Very nice, thank you very much!

I'll make sure to check it out.

I'm using the problems tab since the beginning and it's really useful.

I’ve added a number of unit tests to ensure these features work as intended. However, since I don’t use these features extensively myself, your feedback is important. If you notice anything that doesn’t work as expected, feel free to open an issue on the [Yamma GitHub repository](https://github.com/glacode/yamma). --

You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

To view this discussion visit https://groups.google.com/d/msgid/metamath/6fa52b40-8862-4bd1-88c2-7d398dd69a46n%40googlegroups.com.

[Glauco]

I recently discovered a handy feature in VSCode: the ability to install previous versions of Yamma. While I haven’t needed to use it yet, it’s reassuring to know that if a buggy version ever slips through, users can easily roll back to a stable release. It’s a great safety net for both developers and users!

Now, let’s dive into what’s new in Yamma 0.0.19:

### Version 0.0.19 (2025-03-19)
#### Added
- **Automatic Generation of Disjoint Variable Constraints**:
  - Introduced a new configuration option `yamma.disjVarAutomaticGeneration` in `package.json` to control the automatic generation of disjoint variable (`$d`) constraints. The available options are:
    - `GenerateNone`: No automatic generation of `$d` statements.
    - `GenerateDummy`: Automatically generates dummy `$d` statements for non-mandatory disjoint variable constraints (default configuration)
    - `GenerateAll`: Automatically generates all required `$d` statements, including mandatory ones.
- **Enhanced README.md Documentation**:
  - **Removed Node.js Prerequisite**: Updated the `README.md` to clarify that Node.js is not required for installation, as it was never a prerequisite.
  - Added **CTRL+R** shortcut for **Unify and Renumber** functionality.
  - Added **CTRL+SPACE** shortcut for **Step Suggestions**.
  - Included **animated GIFs** to demonstrate:
    - **Syntax Suggestions** feature.
    - **Step Suggestions** feature.

### Improve
- Diagnostic for missing $d statements is now divided in **mandatory** and **dummy**
  - Code actions are distinct for both cases
- Quick fixes now keep clearly separated newly generated $d statements
- At the bottom of the proof, $d statements are **automatically classified in mandatory or dummy**
  - Within each group, $d statements are now reordered alphabetically
- Eliminated redundant $d constraints to improve consistency and readability of constraint declarations

### Fix
- Prevent multiple theory loads when mmFileFullPath is empty and the semantic tokenization is triggered while the TheoryLoader is still processing
- Fix **semantic tokenization** timing:
      - Perform semantic tokenization just after the theory is downloaded.
      - Ensure tokenization is correctly triggered when a tab is clicked.

### Performance
- **Optimized Test Suite Execution**: Introduced the `--runInBand` parameter to enhance performance by running tests sequentially, preventing resource depletion and improving stability during test execution.
- MmpParser.mandatoryVars is now computed once and cached