]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/tests/TPTP/fetch_results_tptp.lua
auto => autobatch
[helm.git] / helm / software / matita / tests / TPTP / fetch_results_tptp.lua
1 #! /usr/bin/lua50
2
3 require "luasocket"
4
5 SYSTEM = "Matita---0.1.0.UNS-Ref.s"
6 URL = "http://www.cs.miami.edu/~tptp/cgi-bin/DVTPTP2WWW/view_file.pl?Category=Solutions&Domain=%s&File=%s&System=%s"
7
8 function url_for(system, problem)
9         local domain = string.sub(problem,1,3)
10         local url = string.format(URL,domain,problem,system)
11         return url
12 end
13
14 function load_todo_list(file)
15         local f = io.open(file,"r")
16         local todo = {}
17         for l in f:lines() do
18                 table.insert(todo,l)
19         end
20         f:close()
21         return todo
22 end
23
24 function main(argv)
25         assert(table.getn(argv) == 1,
26                 "Only one paarmeter: the file containing the problems")
27         local todo = load_todo_list(argv[1])
28         local todo_size = table.getn(todo)
29         for i=1,todo_size do
30                 local filename = todo[i]
31                 local url = url_for(SYSTEM,filename)
32                 print("Fetching "..filename.." ("..i.."/"..todo_size..") "..url)
33                 local data,err = socket.http.get(url)
34                 assert(data,err)
35                 local logfilename = "log."..filename
36                 local f = io.open(logfilename,"w")
37                 f:write(data)
38                 f:close()
39                 os.execute("gzip -f "..logfilename)
40         end
41 end
42
43 main(arg)