search

UniFormal / MMT

The MMT Language and System
https://uniformal.github.io/
Other
68 stars 23 forks source link

isabelle: fix ULO namepsace #521

Open kissen opened 4 years ago

kissen commented 4 years ago

This patch fixes a typo in the XML namespace in the Isabelle exporter. If you look at the ontology file you see that the XML namespace ends with a hash.

tkw1536 commented 4 years ago

LGTM, I think the test failures are not related to the changes introduced.

tkw1536 commented 4 years ago

@florian-rabe FYI this is coming from the student working on tetrapodal search.

kohlhase commented 4 years ago

Why has this not been merged? Was this just forgotten?

florian-rabe commented 4 years ago

Which # is it?

Is the # the bug or the fix?

Jazzpirate commented 4 years ago

Which # is it?

Is the # the bug or the fix?

The # is the "bug" - Isabelle uses that (if I remember correctly) as a separator between a name and it's "declaration type"; e.g. "zero#constant", "Nat#type" etc.

kissen commented 4 years ago

Which # is it? Is the # the bug or the fix?

The # is the "bug" - Isabelle uses that (if I remember correctly) as a separator between a name and it's "declaration type"; e.g. "zero#constant", "Nat#type" etc.

Is that a problem? I believe all this patch changes is the emitted namespace. Any more hashes afterwards in an URIs should not be a problem(?)

The problem from what I understand is just that the namespace that's being emitted is missing the hash, so we get https://mathhub.info/ulofoobar in the XML files, rather than the intended https://mathhub.info/ulo#foobar.