From 21294064f37343c251282adc3bb60cb2623db410 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20Sch=C3=A4rtl?= <andreas@schaertl.me>
Date: Mon, 27 Apr 2020 17:44:19 +0200
Subject: [PATCH] week18.txt: the IRIs in the Isabelle exports are illegal

- find out how to fix them

- probably should contact whoever did this to fix it as well; look
  at ULO paper again, look at how big this problem is
---
 timeline/week18.txt | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/timeline/week18.txt b/timeline/week18.txt
index be0dcb3..a59125a 100644
--- a/timeline/week18.txt
+++ b/timeline/week18.txt
@@ -27,8 +27,20 @@ Week 18 (27.04.-03.05.)
 		-> 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)
+
 	[ ] run all quries from ulo paper in graphdb
 
+[ ] fix exported IRIs
+
 [ ] familiarize w/ MathHub infastructure
 
 	[ ] look at tooling; user interface &c
-- 
GitLab