From 28778a754f191b4d3f181b83f538b7f00b9c16a0 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 17 Apr 2021 20:59:15 +0200 Subject: [PATCH] [sertop] Add Python interface using pythonlib This PR adds a python interface to the SerAPI protocol using `pythonlib`, which allows to call OCaml functions from Python. Current setup is based on https://github.com/jonathan-laurent/pyml_example , thanks a lot! But a lot more work is needed in order for this to be useful and to adhere to Python conventions. Requires pinning `ppx_python` to commit https://github.com/janestreet/ppx_python/commit/86db99c4b3ebb3c3330c582518c33c9e80b24ddb Closes: #48 --- Makefile | 9 ++ serapi/serapi_protocol.ml | 8 +- serpyc/__init__.py | 16 ++++ serpyc/coqpyc.ml | 168 ++++++++++++++++++++++++++++++++++++++ serpyc/dune | 5 ++ setup.py | 12 +++ test.py | 28 +++++++ 7 files changed, 244 insertions(+), 2 deletions(-) create mode 100644 serpyc/__init__.py create mode 100644 serpyc/coqpyc.ml create mode 100644 serpyc/dune create mode 100644 setup.py create mode 100644 test.py diff --git a/Makefile b/Makefile index 2c7cb5a9..efa4c321 100644 --- a/Makefile +++ b/Makefile @@ -72,6 +72,15 @@ js-dist: js-release: rsync -avp --exclude=*~ --exclude=.git --exclude=README.md --exclude=get-hashes.sh --delete js/ ~/research/jscoq-builds +# Python +.PHONY: python + +PYNAME=coqpyc + +python: + dune build serpyc/$(PYNAME).so setup.py test.py + ( cd _build/default && python3 setup.py build && pip3 install . ) + ##################################################### # Misc diff --git a/serapi/serapi_protocol.ml b/serapi/serapi_protocol.ml index 046db956..df1c710f 100644 --- a/serapi/serapi_protocol.ml +++ b/serapi/serapi_protocol.ml @@ -675,6 +675,8 @@ let coq_exn_info exn = ; str = Pp.string_of_ppcmds pp } +let d c = Format.eprintf "component: %s@\n%!" c + (* Simple protection for Coq-generated exceptions *) let coq_protect st e = try e () @ [Completed], st @@ -889,6 +891,7 @@ let exec_cmd (st : State.t) (cmd : cmd) : answer_kind list * State.t = let doc = Stm.get_doc !doc_id in coq_protect st @@ fun () -> match cmd with | NewDoc opts -> + d "newdoc"; let stm_options = Stm.AsyncOpts.default_opts in let require_libs = Option.default (["Coq.Init.Prelude", None, Some true]) opts.require_libs in let dft_ml, dft_vo = @@ -918,12 +921,13 @@ let exec_cmd (st : State.t) (cmd : cmd) : answer_kind list * State.t = Serapi_doc.save_vo ~doc ~pstate ~in_file ?ldir:st.ldir; [] end | Add (opt, s) -> + d ("add: " ^ s); let _doc, pa, res = ControlUtil.add_sentences ~doc opt s in QueryUtil.add_comments pa; res | Cancel stms -> List.concat @@ List.map (fun x -> snd @@ ControlUtil.(cancel_sentence ~doc x)) stms - | Exec st -> ignore(Stm.observe ~doc st); [] - | Query (opt, qry) -> [ObjList (exec_query opt qry)] + | Exec st -> d "exec"; ignore(Stm.observe ~doc st); [] + | Query (opt, qry) -> d "query"; [ObjList (exec_query opt qry)] | Print(opts, obj) -> let st = Stm.state_of_id ~doc opts.sid in let sigma, env = context_of_st st in diff --git a/serpyc/__init__.py b/serpyc/__init__.py new file mode 100644 index 00000000..e86bccbf --- /dev/null +++ b/serpyc/__init__.py @@ -0,0 +1,16 @@ +""" +Coq Python bindings +""" + +import os +from ctypes import PyDLL, RTLD_GLOBAL, c_char_p + +curdir = dir_path = os.path.dirname(os.path.realpath(__file__)) +dll = PyDLL(f"{curdir}/coqpyc.so", RTLD_GLOBAL) +argv_t = c_char_p * 2 +argv = argv_t("coqpyc.so".encode('utf-8'), None) +dll.caml_startup(argv) + +# We export the names explicitly otherwise mypy gets confused and +# generates spurious errors +# from serpyc import coq diff --git a/serpyc/coqpyc.ml b/serpyc/coqpyc.ml new file mode 100644 index 00000000..557d9a3a --- /dev/null +++ b/serpyc/coqpyc.ml @@ -0,0 +1,168 @@ +open Base +open Python_lib + +module SP = Serapi.Serapi_protocol +module SY = Sertop.Sertop_pyser +module D = Defunc + +module CParam : sig + val sid : Stateid.t D.Of_python.t + val coq_object : SP.coq_object D.Of_python.t + val add_opts : SP.add_opts D.Of_python.t + val query_opt : SP.query_opt D.Of_python.t + val query_cmd : SP.query_cmd D.Of_python.t + val print_opt : SP.print_opt D.Of_python.t +end = struct + let sid = D.Of_python.create ~type_name:"sid" ~conv:SY.Stateid.t_of_python + let coq_object = D.Of_python.create ~type_name:"coq_object" ~conv:SY.coq_object_of_python + let add_opts = D.Of_python.create ~type_name:"add_opts" ~conv:SY.add_opts_of_python + let query_opt = D.Of_python.create ~type_name:"query_opt" ~conv:SY.query_opt_of_python + let query_cmd = D.Of_python.create ~type_name:"query_cmd" ~conv:SY.query_cmd_of_python + let print_opt = D.Of_python.create ~type_name:"print_opt" ~conv:SY.print_opt_of_python +end + +let wrap f = + try f () + with exn -> + let str = Caml.Printexc.to_string exn in + Python_lib.python_of_string str + +let exec_cmd = + let st_ref = ref (SP.State.make ()) in + fun cmd -> + let ans, st = SP.exec_cmd !st_ref cmd in + st_ref := st; + ans + +(* XXX: use applicative syntax *) +let coq_add : pyobject D.t = + let open D.Param in + let open CParam in + let code = positional "code" string ~docstring:"Coq code to parse" in + let opts = positional "opts" add_opts ~docstring:"add options" in + Defunc.map2 code opts ~f:(fun code opts -> + wrap @@ fun () -> + let cmd = SP.Add (opts, code) in + let ans = exec_cmd cmd in + Python_lib.python_of_list SY.python_of_answer_kind ans + ) + +let coq_exec : pyobject D.t = + let open D.Param in + let open CParam in + let sid = positional "sid" sid ~docstring:"sid to reach" in + Defunc.map sid ~f:(fun sid -> + wrap @@ fun () -> + let cmd = SP.Exec sid in + let ans = exec_cmd cmd in + Python_lib.python_of_list SY.python_of_answer_kind ans + ) + +let coq_query : pyobject D.t = + let open D.Param in + let open CParam in + let cmd = positional "cmd" query_cmd ~docstring:"query command" in + let opts = positional "opts" query_opt ~docstring:"query options" in + Defunc.map2 opts cmd ~f:(fun opts cmd -> + wrap @@ fun () -> + let cmd = SP.Query(opts,cmd) in + Caml.Format.eprintf "going to call query@\n%!"; + let ans = exec_cmd cmd in + Python_lib.python_of_list SY.python_of_answer_kind ans + ) + +let coq_print : pyobject D.t = + let open D.Param in + let open CParam in + let obj = positional "obj" coq_object ~docstring:"Coq object to print" in + let opts = positional "opts" print_opt ~docstring:"print options" in + Defunc.map2 obj opts ~f:(fun obj opts -> + wrap @@ fun () -> + let cmd = SP.Print(opts,obj) in + Caml.Format.eprintf "going to call print@\n%!"; + let ans = exec_cmd cmd in + Python_lib.python_of_list SY.python_of_answer_kind ans + ) + +let coq_init () = + let open Sertop.Sertop_init in + + let fb_handler fmt (fb : Feedback.feedback) = + let open Feedback in + let open Caml.Format in + let pp_lvl fmt lvl = match lvl with + | Error -> fprintf fmt "Error: " + | Info -> fprintf fmt "Info: " + | Debug -> fprintf fmt "Debug: " + | Warning -> fprintf fmt "Warning: " + | Notice -> fprintf fmt "" + in + let pp_loc fmt loc = let open Loc in match loc with + | None -> fprintf fmt "" + | Some loc -> + let where = + match loc.fname with InFile f -> f | ToplevelInput -> "Toplevel input" in + fprintf fmt "\"%s\", line %d, characters %d-%d:@\n" + where loc.line_nb (loc.bp-loc.bol_pos) (loc.ep-loc.bol_pos) in + match fb.contents with + | Processed -> + fprintf fmt "Processed@\n%!" + | ProcessingIn s -> + fprintf fmt "Processing in %s@\n%!" s + | FileLoaded (m,n) -> + fprintf fmt "file_loaded: %s, %s@\n%!" m n + | Message (lvl,loc,msg) -> + fprintf fmt "@[%a@]%a@[%a@]\n%!" pp_loc loc pp_lvl lvl Pp.pp_with msg + | _ -> () + in + + (* coq initialization *) + coq_init + { fb_handler + ; ml_load = None + ; debug = true + ; allow_sprop = true + ; indices_matter = false + } Caml.Format.err_formatter; + + (* document initialization *) + + let stm_options = Stm.AsyncOpts.default_opts in + + (* Disable due to https://github.com/ejgallego/coq-serapi/pull/94 *) + let stm_options = + { stm_options with + async_proofs_tac_error_resilience = `None + ; async_proofs_cmd_error_resilience = false + } in + + let injections = [Stm.RequireInjection ("Coq.Init.Prelude", None, Some false)] in + + let dft_ml_path, vo_path = + Serapi.Serapi_paths.coq_loadpath_default ~implicit:true ~coq_path:Coq_config.coqlib in + let ml_load_path = dft_ml_path in + let vo_load_path = vo_path in + + let sertop_dp = Names.(DirPath.make [Id.of_string "PyTop"]) in + let doc_type = Stm.Interactive (TopLogical sertop_dp) in + + let ndoc = { Stm.doc_type + ; injections + ; ml_load_path + ; vo_load_path + ; stm_options + } in + + let _ = Stm.new_doc ndoc in + Caml.Format.eprintf "🐓🐓 Coq's initialization complete 🐓🐓@\n%!" + +let () = + if not (Py.is_initialized ()) + then Py.initialize (); + let () = coq_init () in + let mod_ = Py_module.create "coq" in + Py_module.set mod_ "add" coq_add; + Py_module.set mod_ "exec" coq_exec; + Py_module.set mod_ "query" coq_query; + Py_module.set mod_ "print" coq_print; + () diff --git a/serpyc/dune b/serpyc/dune new file mode 100644 index 00000000..ec7aebf1 --- /dev/null +++ b/serpyc/dune @@ -0,0 +1,5 @@ +(executable + (name coqpyc) + (modes (native shared_object)) + (flags :standard -linkall) + (libraries pythonlib coq-serapi.serapi_v8_13 coq-serapi.sertop_v8_12)) diff --git a/setup.py b/setup.py new file mode 100644 index 00000000..115c6ae6 --- /dev/null +++ b/setup.py @@ -0,0 +1,12 @@ +from distutils.core import setup + +NAME = "serpyc" + +setup( + name=NAME, + version="0.0.1", + author="Jonathan Laurent", + author_email="Jonathan.laurent@cs.cmu.edu", + description="A small example package", + packages=[NAME], + package_data={NAME: ['coqpyc.so']}) diff --git a/test.py b/test.py new file mode 100644 index 00000000..b2e6c0f3 --- /dev/null +++ b/test.py @@ -0,0 +1,28 @@ +import serpyc, coq + +print("step1") +opts = {"newtip": 2, "ontop": 1, "lim": 10 } +res = coq.add("Definition a := 3.", opts) +print(res) + +print("step2") +opts = {"newtip": 3, "ontop": 2, "lim": 10 } +res = coq.add("Definition b := 2.", opts) +print(res) + +print("step3") +res = coq.exec(3) +print(res) + +print("step4") +ppopts = { "pp_format": ("PpSer",None), "pp_depth": 1000, "pp_elide": "...", "pp_margin": 90} +opts = {"limit": 100, "preds": [], "sid": 3, "pp": ppopts, "route": 0} +cmd = ('Ast',None) +res = coq.query(opts, cmd) +print(res) + +print("step5") +obj = res[0][1][0][0] +opts = { "pp": { "pp_format": ("PpStr",None) } } +res = coq.print(obj, opts) +print(res)