chapar
chapar copied to clipboard
coq-community
Unix.Unix_error while running ./batchrundetach
Hi,
I cloned the project from git and ran make, make install and make stores, which all seemed well. But I ran the demo experiment with ./batchrundetach and it returned the following error:
Run: 1 Launching ... Tue Jul 13 10:13:09 MDT 2021 Fatal error: exception Unix.Unix_error(Unix.EINVAL, "out_channel_of_descr", "") Receiving and saving results ... scp: /root/Runner/Worker0/Result.txt: No such file or directory scp: /root/Runner/Worker1/Result.txt: No such file or directory scp: /root/Runner/Worker2/Result.txt: No such file or directory scp: /root/Runner/Worker3/Result.txt: No such file or directory cat: 'Result*': No such file or directory Results ... rm: cannot remove 'Result*': No such file or directory Sleeping for 10 seconds before the next run ...
The following configurations FYI:
Settings.txt KeyRange= 50 RepeatCount= 2 LauncherNode= [email protected] MasterNode= [email protected] WorkerNodes= [email protected] [email protected] [email protected] [email protected]
Packages under opam:
Packages matching: installed Name Installed Synopsis base-bigarray base base-threads base base-unix base batteries 3.3.0 A community-maintained standard library extension conf-findutils 1 Virtual package relying on findutils conf-gmp 3 Virtual package relying on a GMP lib system installation coq 8.13.2 Formal proof management system num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic ocaml 4.12.0 The OCaml compiler (virtual package) ocaml-base-compiler 4.12.0 Official release 4.12.0 ocaml-config 2 OCaml Switch Configuration ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled ocamlbuild 0.14.0 OCamlbuild is a build system with builtin rules to easily build most OCaml projects. ocamlfind 1.9.1 A library manager for OCaml zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers
Could anyone give any suggestions on this?
Sorry, I have no idea what this is about (I know very little about this package actually).
Im having the same issue "Fatal error: exception Unix.Unix_error(Unix.EINVAL, "out_channel_of_descr", "")". The first run seems all good, while the second run always fails... Any idea?
My main goals with maintaining this project are to (1) make sure the Coq code compiles and (2) make sure the extracted code can be compiled. Any non-compilation bugs in the OCaml code, especially the socket-reliant parts, are unfortunately very unlikely to be investigated or fixed by me anytime soon. On the other hand, fixes to this code are welcome as pull requests.
