search

coq-community / chapar

A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]
MIT License
32 stars 7 forks source link

Unix.Unix_error while running ./batchrundetach #21

Open SuperLeilia opened 3 years ago

SuperLeilia commented 3 years ago

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= root@127.0.0.1 MasterNode= root@127.0.0.1 WorkerNodes= root@127.0.0.1 root@127.0.0.1 root@127.0.0.1 root@127.0.0.1

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?

SuperLeilia commented 3 years ago

@palmskog @Zimmi48

Zimmi48 commented 3 years ago

Sorry, I have no idea what this is about (I know very little about this package actually).

siliunobi commented 3 years ago

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?

palmskog commented 3 years ago

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.