Migrate from ST4 to Apache Freemarker in keyext.proofmanagement

[wadoon]

Related Issue

ST4 is blocking from module-info usage, see #3451.
This PR swaps ST4 against Apache Freemarker.

Type of pull request

• Refactoring (behaviour should not change or only minimally change)

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I added new test case(s) for new functionality.

[WolframPfeifer]

On my branch pfeifer/rmst I fixed the report generation. I reverted some changes you did, for example moving CheckerDate.ProofEntry from an inner (non-static!) class into a top-level class. It is not pretty, but seems to work there now.

[WolframPfeifer]

On my branch pfeifer/rmst I fixed the report generation. I reverted some changes you did, for example moving CheckerDate.ProofEntry from an inner (non-static!) class into a top-level class. It is not pretty, but seems to work there now.

Ah no, spoke too soon! Some things are still wrong in the report (filtering of messages, settings entries, CSS) ...
But at least there is no Freemarker exception any more.

[wadoon]

Ah no, spoke too soon! Some things are still wrong in the report (filtering of messages, settings entries, CSS) ... But at least there is no Freemarker exception any more.

With f3459ad, the report is generated successfully w/o exception.
I cherry-picked your branch, made some smaller adjustments, and already added #3622. It should be fine now.

Rebase required, before merge.

[WolframPfeifer]

In 1bbc18a on pfeifer/rmstJS, I reverted to the original JS functionality for the tabs. The current CSS variant had the (imo serious) drawback, that it always jumped down to the "beginning" of the tab and the tab buttens were not visible any more. Also, I fixed the progress bar. Some layout things still need to be fixed, also the table of settings.

[wadoon]

Also, I fixed the progress bar

I did this on purpose. The format of a cumulative bar chart was misleading: If category "proven" is zero, it is hidden. Reporting should make the current state explicitly visible.

[WolframPfeifer]

Also, I fixed the progress bar

I did this on purpose. The format of a cumulative bar chart was misleading: If category "proven" is zero, it is hidden. Reporting should make the current state explicitly visible.

I thought that the idea of this PR was to do only refactoring and rewriting from ST to Freemarker (as indicated in the description). I would prefer not mixing in functional changes, since the PR is already large enough and should only have one purpose.

Also, in my opinion the "overview bar" in the report is good as is: The number of proofs in the bundle is split between "proven", "dependencies left", and "unproven", if either of these is 0, it is not displayed. In any case, I think the version on main is way easier to read than the one of this PR.

On main:

This PR:

[wadoon]

Also, I fixed the progress bar

I did this on purpose. The format of a cumulative bar chart was misleading: If category "proven" is zero, it is hidden. Reporting should make the current state explicitly visible.

I thought that the idea of this PR was to do only refactoring and rewriting from ST to Freemarker (as indicated in the description). I would prefer not mixing in functional changes, since the PR is already large enough and should only have one purpose.

Also, in my opinion the "overview bar" in the report is good as is: The number of proofs in the bundle is split between "proven", "dependencies left", and "unproven", if either of these is 0, it is not displayed. In any case, I think the version on main is way easier to read than the one of this PR.

You should not hide crucial information. The first time I looked at the report, I did not understand it. It was unclear whether the two categories showed meant something was ok or not. Only by showing "proven: 0", I understood that the category "dependencies left" symbolizes a not-good state.

The problem of hiding information, especially on complex formats, could also result from an error in the output, e.g., the HTML could be corrupt. Printing zero values helps here for auditability. In the end, the report should be simple, convincing and trustworthy.

This PR:

I tried to get this right with your stacked bar chart, but failed to get a good look at low numbers. Also thought of drawing an SVG diagram.