week18.txt

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