X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Ftests%2FTPTP%2Ffetch_results_tptp.lua;fp=matita%2Ftests%2FTPTP%2Ffetch_results_tptp.lua;h=87aa91a98a75a80314f41d15b66bbdab289f04ef;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/matita/tests/TPTP/fetch_results_tptp.lua b/matita/tests/TPTP/fetch_results_tptp.lua
new file mode 100755
index 000000000..87aa91a98
--- /dev/null
+++ b/matita/tests/TPTP/fetch_results_tptp.lua
@@ -0,0 +1,43 @@
+#! /usr/bin/lua50
+
+require "luasocket"
+
+SYSTEM = "Matita---0.1.0.UNS-Ref.s"
+URL = "http://www.cs.miami.edu/~tptp/cgi-bin/DVTPTP2WWW/view_file.pl?Category=Solutions&Domain=%s&File=%s&System=%s"
+
+function url_for(system, problem)
+	local domain = string.sub(problem,1,3)
+	local url = string.format(URL,domain,problem,system)
+	return url
+end
+
+function load_todo_list(file)
+	local f = io.open(file,"r")
+	local todo = {}
+	for l in f:lines() do
+		table.insert(todo,l)
+	end
+	f:close()
+	return todo
+end
+
+function main(argv)
+	assert(table.getn(argv) == 1,
+		"Only one paarmeter: the file containing the problems")
+	local todo = load_todo_list(argv[1])
+	local todo_size = table.getn(todo)
+	for i=1,todo_size do
+		local filename = todo[i]
+		local url = url_for(SYSTEM,filename)
+		print("Fetching "..filename.." ("..i.."/"..todo_size..") "..url)
+		local data,err = socket.http.get(url)
+		assert(data,err)
+		local logfilename = "log."..filename
+		local f = io.open(logfilename,"w")
+		f:write(data)
+		f:close()
+		os.execute("gzip -f "..logfilename)
+	end
+end
+
+main(arg)