Skip to content

isabelle: fix ULO namepsace#521

Open
kissen wants to merge 1 commit into
UniFormal:develfrom
kissen:fix/isabelle-namespace
Open

isabelle: fix ULO namepsace#521
kissen wants to merge 1 commit into
UniFormal:develfrom
kissen:fix/isabelle-namespace

Conversation

@kissen

@kissen kissen commented Jun 9, 2020

Copy link
Copy Markdown

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

tkw1536 commented Jun 14, 2020

Copy link
Copy Markdown
Contributor

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

@tkw1536

tkw1536 commented Jun 14, 2020

Copy link
Copy Markdown
Contributor

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

@kohlhase

kohlhase commented Jul 8, 2020

Copy link
Copy Markdown
Member

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

@florian-rabe

Copy link
Copy Markdown
Member

Which # is it?

Is the # the bug or the fix?

@Jazzpirate

Copy link
Copy Markdown
Contributor

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

kissen commented Jul 9, 2020

Copy link
Copy Markdown
Author

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

5 participants