dwhalen / holophrasm

Holophrasm: a neural Automated Theorem Prover for higher-order logic
MIT License
51 stars 13 forks source link

Run on Windows #1

Open thepok opened 7 years ago

thepok commented 7 years ago

Hello,i tried to run it in Windows, but i get

C:\Users\Marcel>python \holophrasm-master\run_script_ordered.py timeout (min)? 1 num passes? 1000 search beam width? 3 hyp bonus? (0 in the paper, but 10 may give better results)0 Traceback (most recent call last): File "C:\Users\Marcel\Desktop\holophrasm-master\run_script_ordered.py", line 57, in with open('lm', 'rb') as handle: IOError: [Errno 2] No such file or directory: 'lm'

I guess this file is just missing in the repo?

dwhalen commented 7 years ago

The release version (https://github.com/dwhalen/holophrasm/releases) should have the missing files. Let me know if that doesn't work.

thepok commented 7 years ago

It works now somewhat, but it spits out

proven 28/389 this: 5, 7.2% proposition onnbtwn (4030): 389/2720 (with 3 steps) Exception in thread 0: Traceback (most recent call last): File "D:\programme\anacondaPY2.7\lib\threading.py", line 801, in bootstrap_inner self.run() File "C:\Users\Marcel\Desktop\holophrasm\holophrasm\proof_search.py", line 180, in run with withPool(1) as self.p: File "C:\Users\Marcel\Desktop\holophrasm\holophrasm\proof_search.py", line 117, in init self.p = multiprocessing.Pool(procs, init_func) File "D:\programme\anacondaPY2.7\lib\multiprocessing__init.py", line 232, in Pool return Pool(processes, initializer, initargs, maxtasksperchild) File "D:\programme\anacondaPY2.7\lib\multiprocessing\pool.py", line 159, in init__ self._repopulate_pool() File "D:\programme\anacondaPY2.7\lib\multiprocessing\pool.py", line 223, in _repopulate_pool w.start() File "D:\programme\anacondaPY2.7\lib\multiprocessing\process.py", line 130, in start self._popen = Popen(self) File "D:\programme\anacondaPY2.7\lib\multiprocessing\forking.py", line 258, in init__ cmd = get_command_line() + [rhandle] File "D:\programme\anacondaPY2.7\lib\multiprocessing\forking.py", line 358, in get_command_line is not going to be frozen to produce a Windows executable.''') RuntimeError: Attempt to start a new process before the current process has finished its bootstrapping phase.

        This probably means that you are on Windows and you have
        forgotten to use the proper idiom in the main module:

            if __name__ == '__main__':
                freeze_support()
                ...

        The "freeze_support()" line can be omitted if the program
        is not going to be frozen to produce a Windows executable.

proven 28/390 this: 5, 7.2%

all the time.

Iam not used to Python, i dont think its a big problem, i hope you can fix it :)