Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

isabelle: fix ULO namepsace #521

Open
wants to merge 1 commit into
base: devel
Choose a base branch
from

Conversation

kissen
Copy link

@kissen kissen commented Jun 9, 2020

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
Copy link
Contributor

tkw1536 commented Jun 14, 2020

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

@tkw1536
Copy link
Contributor

tkw1536 commented Jun 14, 2020

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

@kohlhase
Copy link
Member

kohlhase commented Jul 8, 2020

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

@florian-rabe
Copy link
Member

Which # is it?

Is the # the bug or the fix?

@Jazzpirate
Copy link
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
Copy link
Author

kissen commented Jul 9, 2020

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