MetaSpace for documentation and origin

[wadoon]

Intended Change

Introduces MetaSpace in alignment with Namespace<T>. A MetaSpace captures the non-proof-relevant information of signature entities, i.e., documentation and origin.

This makes the ncore definitions simpler and enables MetaSpace to be shuttable for performance.

The MetaSpace is filled by the DeclarationBuilder & Co using the DOC_COMMENT given in KeY files. Therefore, the description of some entities in XML becomes obsolete. The relevant descriptions were migrated. Now, InfoTree shows every known function in the goal.

Type of pull request

• Refactoring (behaviour should not change or only minimally change)
• New feature (non-breaking change which adds functionality)

Ensuring quality

• I have tested the feature as follows: unit-tests

[wadoon]

@FliegendeWurst

I stumbled across the following lines in keyext.caching. This PR breaks the lines, and I tried to repair it. But overall, for me, the concept is very bogus. The origin was only meant for user support, and is not meant to be reliable or always present. I guess your algorithm can be tricked by using \include of user-defined KeY files.

Please revise the lines so that it uses robust markers and not origin. And maybe rewrite the code to be more readable...

/cc @WolframPfeifer

[FliegendeWurst]

Please revise the lines so that it uses robust markers and not origin.

Are there other markers to indicate that a taclet is user-defined? I had a quick look at the taclets in a debugger and could not spot other fields that would help.

Alternatively the check could be removed. For the common case of using the same user-defined taclets in all proofs of the same session it does not matter.

[wadoon]

Are there other markers to indicate that a taclet is user-defined? I had a quick look at the taclets in a debugger and could not spot other fields that would help.

This differentiation does not make sense to me. There is nothing special whether Taclets were loaded b/c of the profile, or by an include in the KeYUserProblemFile.

If you want to find out whether a taclet proof-specific, you need to look up in the init configs.

Alternatively the check could be removed. For the common case of using the same user-defined taclets in all proofs of the same session it does not matter.

What defines the identity of a Taclet? If the same Taclet (by syntax) is given in two proof files, is it the same Taclet? KeY copies the declaration header always, but does not copy included files.

Also, equality by syntax is difficult, as Taclet options can deactivate goal templates.

I see a conceptual hole.