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)