### 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). -- 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 [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/6fa52b40-8862-4bd1-88c2-7d398dd69a46n%40googlegroups.com.
