From 79b7460cfba407deb8544277680776d92c331eb4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20Sch=C3=A4rtl?= <andreas@schaertl.me>
Date: Wed, 17 Jun 2020 15:18:42 +0200
Subject: [PATCH] experimental/ulo: explain problems with data properties

---
 experimental/ulo/coq-export-bugs.txt | 39 ++++++++++++++++++++++++----
 1 file changed, 34 insertions(+), 5 deletions(-)

diff --git a/experimental/ulo/coq-export-bugs.txt b/experimental/ulo/coq-export-bugs.txt
index 2840e85..404cd7b 100644
--- a/experimental/ulo/coq-export-bugs.txt
+++ b/experimental/ulo/coq-export-bugs.txt
@@ -1,7 +1,36 @@
-- tags that shouldn't be there, i.e. `Target`, `HasInHypothesis` and
-  so on
+The Coqxml [1] exports have some bugs.
 
-- wrong ULO namespace
+* The RDF files contain tags that should not be there. For example,
+  `<Target>`, `<HasInHypothesis>` and so on.
 
-- objects have relative URIs which is annoying; this might be annoying
-  but it is not a bug
+* The ULO namespace is wrong. It should be
+
+    https://mathhub.info/ulo#
+
+  as defined in the ontology file [2].
+
+* Handling of data properties seems wrong. Data properties are
+
+    `ulo:sourceref`, `ulo:docref` and `ulo:internal-size`
+
+  as well as some imported dcterms, that is
+
+    `dcterms:title` and `dcterms:isVersionOf`
+
+  In the Coqxml exports, these are used together with references,
+  e.g.
+
+    <ulo:docref rdf:resource="Coq.Arith.Between.html#bet_eq" />
+    <ulo:sourceref rdf:resource="32" />
+
+  but RDF/XML requires the rdf:resource to be an IRI. Here, this is
+  not the case. A standard-compliant example of the code above should
+  like like this
+
+    <ulo:docref>Coq.Arith.Between.html#bet_eq</ulo:docref>
+    <ulo:sourceref>32</ulo:sourceref>
+
+  which makes the values literals.
+
+[1] https://gl.mathhub.info/Coqxml
+[2] https://gl.mathhub.info/ulo/ulo/-/blob/master/ulo.owl
-- 
GitLab