Quick answer: replace 'Driver.load_driver_absolute' by 'Whyconf.load_driver'
My first reaction was: why not following the doc properly? (http://why3.lri.fr/doc/api.html#sec28) However, I agree that the doc is outdated, sorry for the inconvenience. The initial recommendation of that doc section is: ``The OCaml code given below is available in the source distribution in directory examples/use_api/ together with a few other examples.''. Indeed, I recommend to look at these files from the source distribution, since their accuracy is maintained when the API involves. In details: "alt_ergo" is the name of the driver file associated to the ALt-Ergo prover in the why3.conf file. This is not an absolute path name, so you need to use Whyconf.load_drive to properly prepend the path of drivers from Why3 library (and indeed also append ".drv" to it). Hope this helps, - Claude Le 29/03/2018 à 00:29, Abhishek Kumar a écrit : > Hello > I am trying to use Why3 API from Ocaml. I am unable to load the alt-ergo > driver. For the below-shown code, I get the error "Failed to load driver > for alt-ergo: anomaly: Sys_error("alt_ergo: No such file or > directory")". I am not sure, where is it looking for which file. I have > alt-ergo installed and configured (the first part of the code succeeds). > > ``` > let alt_ergo : Whyconf.config_prover = > try > let prover = {Whyconf.prover_name = "Alt-Ergo"; > prover_version = "1.30"; > prover_altern = ""} in > Whyconf.Mprover.find prover provers > with Not_found -> > Printf.printf "Prover alt-ergo not installed or not configured@."; > exit 0 > > > let alt_ergo_driver : Driver.driver = > try > Driver.load_driver_absolute env alt_ergo.Whyconf.driver [] > with e -> > eprintf "Failed to load driver for alt-ergo: %a@." > Exn_printer.exn_printer e; > exit 1 > ``` > > Can someone please help me how to get this working? > > Thanks a lot! > Abhishek > > > _______________________________________________ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club > -- Claude Marché | tel: +33 1 69 15 66 08 INRIA Saclay - Île-de-France | Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex | _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
