Week 18 (27.04.-03.05.) ======================= [~] familiarize yourself w/ some tooling [x] run all queries from ulo paper in virtuoso [~] import all data into graphdb [x] import coq data into graphdb -> had to use a little scritping to remove some invalid(?!) parts from the rdf files -> used script /ulo/coq-cut.sh [~] import isabelle data into graphdb -> importing the isabelle rdf files I get an error org.eclipse.rdf4j.sail.SailException: Invalid IRI value for all files; I wonder if the proposed IRI scheme is actually illegal; will have to look into that -> RDF [1] uses IRIs which "are a generialization of URI [2]"; IRIs are also defined by the IETF [3] -> looking at the grammar of IRIs [3], it indeed seems like the pipe symbol as used by the ULO exports is in fact not allowed in IRIs; to quote the IRI grammar iunreserved = ALPHA / DIGIT / "-" / "." / "_" / "~" / ucschar where ucschar defines various regions of unicode characters; the lowest of the range is 0xa0, which is below 0x7c (the pipe symbol) -> the IRIs in the Isabelle exports have the following characters which are (according to automated tool `iriok' [4]) not valid: '|', '\', ' ', '^' -> importing the files w/ fixed IRIs I get new errors from graphDB (sigh) RDF Parse Error: The processing instruction target matching "[xX][mM][IL}' is not allowed e.g. w/ file Flow_Networks.Graph_Impl.rdf.gz [ ] run all quries from ulo paper in graphdb [ ] fix exported IRIs [ ] familiarize w/ MathHub infastructure [ ] look at tooling; user interface &c [ ] look at programming interfaces [ ] evaluate databases for integration w/ MathHub References ========== [1] https://www.w3.org/TR/2014/REC-rdf11-concepts-20140225/ [2] https://tools.ietf.org/html/rfc3986 [3] https://tools.ietf.org/html/rfc3987 [4] https://gitlab.cs.fau.de/kissen/iriok