Brando Miranda

why doesn't this work: ``` (Print ((sid 6) (pp ((pp_format PpStr)))) (CoqGenArg (GenArg raw (ExtraArg tactic) (TacArg (Reference ((v (Ser_Qualid (DirPath ()) (Id O))) (loc (((fname ToplevelInput) (line_nb 1) (bol_pos...

why does the above fail but this work? ``` (Print ((sid 6) (pp ((pp_format PpStr)))) ( CoqGenArg (GenArg raw (ExtraArg tactic) (TacArg ((v (TacCall ((v (((v (Ser_Qualid (DirPath ()) (Id...

I want to traverse arbitrary cast trees and extract whatever argument/part I want and get it back as a coq human string.

@ejgallego is there a way to extend serapi to do this? I am sort of doing it in a very hacky way where I insert a `Show Proof.` statement in...

> It shouldn't be hard to extend indeed, you can call `Proof.partial_proof` to return the term, which can just then be serialized normally. > > I've implemented that in #271,...

@ejgallego thanks emilio! Will test it in a bit. Question on the formal OCaml code modeling for kernel terms vs CoqAsts. A proof term can be something as simple as...

> Note something about opam, you can use `opam pin add coq-serapi https://github.com/ejgallego/coq-serapi#v8.16+show_proof` to actually have opam install my branch and test locally. Btw, I think that didn't work I...

hmmm another error: ``` brandomiranda~ ❯ opam pin add coq-serapi https://github.com/ejgallego/coq-serapi.git#v8.16+show_proof Processing: [coq-serapi.8.11.0+0.11.0: git] Processing: [coq-serapi.8.11.0+0.11.0: git] [coq-serapi.8.11.0+0.11.0] synchronised (git+https://github.com/ejgallego/coq-serapi.git#v8.16+show_proof) coq-serapi is now pinned to git+https://github.com/ejgallego/coq-serapi.git#v8.16+show_proof (version 8.11.0+0.11.0) The following...

hmmm...I think I prefer to use the coq version I have or idk if my project will work...will have to think about it. ---- note for me, need to modify...

I am interested in a Python way to use SerAPI. At what stage is this? I have 4 questions/ideas: * 1) Is there python interface version I can try? *...