search

ejgallego / coq-serapi

Coq Protocol Playground with Se(xp)rialization of Internal Structures.
Other
128 stars 39 forks source link

Querying proof term directly with `Query` #270

Closed brando90 closed 2 years ago

brando90 commented 2 years ago

I tried this interaction:

(Add () "Lemma addn0 n : 0 + n = n. Proof. intros. simpl.")
(Exec 5)
(Query ((pp ((pp_format PpStr)))) Proof)

but I don't get to see the proof term (ideally in human form). Why is that? Am I doing it wrong?

I see:

(Answer 3 Ack)
(Answer 3 (ObjList ((CoqString "FIXME UPSTREAM, provide pr_proof"))))
(Answer 3 Completed)
(Query () Proof)
(Answer 4 Ack)
(Answer 4 (ObjList ((CoqProof ((Ser_Evar 8)) () () ()))))
(Answer 4 Completed)

but expected something like this:

(fun n : nat => ?Goal : 0 + n = n)
ejgallego commented 2 years ago

This indeed needs to be fixed, it is showing the current goal which of course it just a hole waiting to be filled.

brando90 commented 2 years ago

@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 my document. Then I receive immediately a Feedback response from serapi with the coq (raw) string. Then I get the raw coq string and give it back to serapi in the parse command to get something like this:

(Parse ((ontop 1)) "Definition id := fun x : nat => x.")
(Answer 2 Ack)
(Answer 2
 (ObjList
  ((CoqAst
    ((v
      ((control ()) (attrs ())
       (expr
        (VernacDefinition (NoDischarge Definition)
         (((v (Name (Id id)))
           (loc
            (((fname ToplevelInput) (line_nb 1) (bol_pos 0) (line_nb_last 1)
              (bol_pos_last 0) (bp 11) (ep 13)))))
          ())
         (DefineBody () ()
          ((v
            (CLambdaN
             ((CLocalAssum
               (((v (Name (Id x)))
                 (loc
                  (((fname ToplevelInput) (line_nb 1) (bol_pos 0)
                    (line_nb_last 1) (bol_pos_last 0) (bp 21) (ep 22))))))
               (Default Explicit)
               ((v
                 (CRef
                  ((v (Ser_Qualid (DirPath ()) (Id nat)))
                   (loc
                    (((fname ToplevelInput) (line_nb 1) (bol_pos 0)
                      (line_nb_last 1) (bol_pos_last 0) (bp 25) (ep 28)))))
                  ()))
                (loc
                 (((fname ToplevelInput) (line_nb 1) (bol_pos 0)
                   (line_nb_last 1) (bol_pos_last 0) (bp 25) (ep 28)))))))
             ((v
               (CRef
                ((v (Ser_Qualid (DirPath ()) (Id x)))
                 (loc
                  (((fname ToplevelInput) (line_nb 1) (bol_pos 0)
                    (line_nb_last 1) (bol_pos_last 0) (bp 32) (ep 33)))))
                ()))
              (loc
               (((fname ToplevelInput) (line_nb 1) (bol_pos 0)
                 (line_nb_last 1) (bol_pos_last 0) (bp 32) (ep 33)))))))
           (loc
            (((fname ToplevelInput) (line_nb 1) (bol_pos 0) (line_nb_last 1)
              (bol_pos_last 0) (bp 17) (ep 33)))))
          ())))))
     (loc
      (((fname ToplevelInput) (line_nb 1) (bol_pos 0) (line_nb_last 1)
        (bol_pos_last 0) (bp 0) (ep 34)))))))))
(Answer 2 Completed)

but this seems a big hacky. Is it hard to extend serapi with this? It feels it should be easy since serapi doesn't have to modify the CoqAST and can just return it in whatever format it is as long as it's a traversable ast is my guess. What do you think?

ejgallego commented 2 years ago

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, please let me know if that works better for you

brando90 commented 2 years ago

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, please let me know if that works better for you

I'm not an expert in coq-serapi (but getting better!) but this looks good too me since EConstr seems to be the Coq AST constructs I want for processing of the terms. The only confusing point to me is that CoqAST's don't wrap values of that same type but instead wrap vernacs/Vernacexpr.vernac_control (which I assume must include additional syntax like Definitions and other things...).

I will need to make those processed terms back into human strings. I assume the only way to do that is to do:

(Print ((pp ((pp_format PpStr)))) (CoqConstr (App (Rel ...) ((Rel ...)))))

or something like that.

Let's merge it so I can opam install the new coq-serapi interface and test it and give feedback! :)

Thanks Emilio.

ejgallego commented 2 years ago

I need to find out where my writing about Coq ASTs is, but indeed:

There are significant differences between the two.

Yes, you should be able to use Print to print a term back, but be sure you pass the sid parameter correctly, also for incomplete terms some weird stuff may happen, Coq usually doesn't print proofs often so that part is a bit untested.

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.

If would be nice if you could test that way and give some feedback before we make a release.

brando90 commented 2 years ago

@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 fun x : nat => x. (e.g. a proof for the theorem nat -> nat) -- which from your comment implies it's of type "kernel term". Thus, it is a bit unclear to me what the difference between CoqAst's vs kernel terms are formally at the level of OCaml since writing fun x : nat => x. seems to be perfectly legal term. Do you mind clarifying that bit -- especially at the level of OCaml data types?

brando90 commented 2 years ago

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 think (sorry not an opam expert if the solution is easy):

brandomiranda~ ❯ opam pin add coq-serapi https://github.com/ejgallego/coq-serapi#v8.16+show_proof
[coq-serapi.8.11.0+0.11.0] fetching sources failed: Unknown archive type: /private/var/folders/_l/ry3nxq4n3753twbdc4dl77800000gn/T/opam-43966-f01c10/coq-serapi
[ERROR] Error getting source from https://github.com/ejgallego/coq-serapi#v8.16+show_proof:
          - Could not extract archive:
            Unknown archive type: /private/var/folders/_l/ry3nxq4n3753twbdc4dl77800000gn/T/opam-43966-f01c10/coq-serapi
ejgallego commented 2 years ago

That's the correct syntax sorry opam pin add coq-serapi https://github.com/ejgallego/coq-serapi.git#v8.16+show_proof

brando90 commented 2 years ago

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 actions will be performed:
  ↻ recompile coq-serapi 8.11.0+0.11.0*
Do you want to continue? [Y/n] y

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><>  🐫
Processing  1/4: [coq-serapi.8.11.0+0.11.0: git]
⬇ retrieved coq-serapi.8.11.0+0.11.0  (git+https://github.com/ejgallego/coq-serapi.git#v8.16+show_proof)
[ERROR] The compilation of coq-serapi.8.11.0+0.11.0 failed at "dune build -p coq-serapi -j 15".

#=== ERROR while compiling coq-serapi.8.11.0+0.11.0 ===========================#
# context     2.1.2 | macos/x86_64 | ocaml-base-compiler.4.09.1 | pinned(git+https://github.com/ejgallego/coq-serapi.git#v8.16+show_proof#3bb19ccb)
# path        ~/.opam/debug_proj_4.09.1/.opam-switch/build/coq-serapi.8.11.0+0.11.0
# command     ~/.opam/opam-init/hooks/sandbox.sh build dune build -p coq-serapi -j 15
# exit-code   1
# env-file    ~/.opam/log/coq-serapi-59285-38f0d1.env
# output-file ~/.opam/log/coq-serapi-59285-38f0d1.out
### output ###
# [...]
# -> required by _build/default/coq-serapi.install
# -> required by alias install
# File "serlib/plugins/ssrmatching/dune", line 6, characters 12-40:
# 6 |  (libraries coq-core.plugins.ssrmatching serlib serlib_ltac sexplib))
#                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
# Error: Library "coq-core.plugins.ssrmatching" not found.
# -> required by library "coq-serapi.serlib.ssrmatching" in
#    _build/default/serlib/plugins/ssrmatching
# -> required by _build/default/META.coq-serapi
# -> required by _build/install/default/lib/coq-serapi/META
# -> required by _build/default/coq-serapi.install
# -> required by alias install

<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><>  🐫
β”Œβ”€ The following actions failed
β”‚ Ξ» build coq-serapi 8.11.0+0.11.0
└─
╢─ No changes have been performed
[NOTE] Pinning command successful, but your installed packages may be out of sync.
ejgallego commented 2 years ago

Pinning does not force the right Coq version, it seems. For that tree you need to install coq.8.16 at least.

ejgallego commented 2 years ago

And the rest of deps, I'd suggest you first install coq-serapi 0.16 , and then pin.

brando90 commented 2 years ago

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 this later:

RUN opam init --disable-sandboxing
# compiler + '_' + coq_serapi + '.' + coq_serapi_pin
RUN opam switch create ocaml-variants.4.07.1+flambda_coq-serapi.8.11.0+0.11.1 ocaml-variants.4.07.1+flambda
RUN opam switch ocaml-variants.4.07.1+flambda_coq-serapi.8.11.0+0.11.1
RUN eval $(opam env)

RUN opam repo add coq-released https://coq.inria.fr/opam/released
# RUN opam pin add -y coq 8.11.0
# ['opam', 'repo', '--all-switches', 'add', '--set-default', 'coq-released', 'https://coq.inria.fr/opam/released']
RUN opam repo --all-switches add --set-default coq-released https://coq.inria.fr/opam/released
RUN opam update --all
RUN opam pin add -y coq 8.11.0

#RUN opam install -y --switch ocaml-variants.4.07.1+flambda_coq-serapi_coq-serapi_8.11.0+0.11.1 coq-serapi 8.11.0+0.11.1
RUN opam install -y coq-serapi

I think should work:

RUN opam init --disable-sandboxing
# compiler + '_' + coq_serapi + '.' + coq_serapi_pin
RUN opam switch create ocaml-variants.4.07.1+flambda_coq-serapi.8.11.0+0.11.1 ocaml-variants.4.07.1+flambda
RUN opam switch ocaml-variants.4.07.1+flambda_coq-serapi.8.11.0+0.11.1
RUN eval $(opam env)

RUN opam repo add coq-released https://coq.inria.fr/opam/released
# RUN opam pin add -y coq 8.11.0
# ['opam', 'repo', '--all-switches', 'add', '--set-default', 'coq-released', 'https://coq.inria.fr/opam/released']
RUN opam repo --all-switches add --set-default coq-released https://coq.inria.fr/opam/released
RUN opam update --all
# RUN opam pin add -y coq 8.11.0
RUN opam pin add -y coq 8.16.0

#RUN opam install -y --switch ocaml-variants.4.07.1+flambda_coq-serapi_coq-serapi_8.11.0+0.11.1 coq-serapi 8.11.0+0.11.1
# RUN opam install -y coq-serapi
RUN opam pin add coq-serapi https://github.com/ejgallego/coq-serapi.git#v8.16+show_proof
ejgallego commented 2 years ago

Indeed compat is a problem, but this particular change should be easy to backport to 8.11 ; I'd be happy to take a PR for that branch.