Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Respect COQPATH in sertop #221

Closed
cpitclaudel opened this issue Jul 30, 2020 · 1 comment · Fixed by ocaml/opam-repository#17070
Closed

Respect COQPATH in sertop #221

cpitclaudel opened this issue Jul 30, 2020 · 1 comment · Fixed by ocaml/opam-repository#17070
Assignees
@ejgallego
Labels
kind: bug kind: enhancement
Milestone
0.11.1

Comments

@cpitclaudel
Copy link
Collaborator

It would be great for sertop to respect COQPATH. Here's a small repro:

$ cd /tmp
$ mkdir coqlibs
$ echo "Definition a := 1." > coqlibs/A.v
$ coqc coqlibs/A.v 
$ COQPATH=/tmp/coqlibs coqtop <<< "Require Import A."
Welcome to Coq 8.11.1 (May 2020)

Coq < 
Coq < 
$ COQPATH=/tmp/coqlibs sertop <<< '("query0"("Add"()"Require Import A.\n"))'
(Feedback((doc_id 0)(span_id 0)(route 0)(contents(FileLoaded Coq.Init.Prelude /home/clement/.opam/4.09.0/lib/coq/theories/Init/Prelude.vo))))
(Feedback((doc_id 0)(span_id 0)(route 0)(contents(FileLoaded Coq.Init.Notations /home/clement/.opam/4.09.0/lib/coq/theories/Init/Notations.vo))))
(Feedback((doc_id 0)(span_id 0)(route 0)(contents(FileLoaded Coq.Init.Logic /home/clement/.opam/4.09.0/lib/coq/theories/Init/Logic.vo))))
(Feedback((doc_id 0)(span_id 0)(route 0)(contents(FileLoaded Coq.Init.Datatypes /home/clement/.opam/4.09.0/lib/coq/theories/Init/Datatypes.vo))))
(Feedback((doc_id 0)(span_id 0)(route 0)(contents(FileLoaded Coq.Init.Logic_Type /home/clement/.opam/4.09.0/lib/coq/theories/Init/Logic_Type.vo))))
(Feedback((doc_id 0)(span_id 0)(route 0)(contents(FileLoaded Coq.Init.Specif /home/clement/.opam/4.09.0/lib/coq/theories/Init/Specif.vo))))
(Feedback((doc_id 0)(span_id 0)(route 0)(contents(FileLoaded Coq.Init.Decimal /home/clement/.opam/4.09.0/lib/coq/theories/Init/Decimal.vo))))
(Feedback((doc_id 0)(span_id 0)(route 0)(contents(FileLoaded Coq.Init.Nat /home/clement/.opam/4.09.0/lib/coq/theories/Init/Nat.vo))))
(Feedback((doc_id 0)(span_id 0)(route 0)(contents(FileLoaded Coq.Init.Byte /home/clement/.opam/4.09.0/lib/coq/theories/Init/Byte.vo))))
(Feedback((doc_id 0)(span_id 0)(route 0)(contents(FileLoaded Coq.Init.Peano /home/clement/.opam/4.09.0/lib/coq/theories/Init/Peano.vo))))
(Feedback((doc_id 0)(span_id 0)(route 0)(contents(FileLoaded Coq.Init.Wf /home/clement/.opam/4.09.0/lib/coq/theories/Init/Wf.vo))))
(Feedback((doc_id 0)(span_id 0)(route 0)(contents(FileLoaded Coq.Init.Tactics /home/clement/.opam/4.09.0/lib/coq/theories/Init/Tactics.vo))))
(Feedback((doc_id 0)(span_id 0)(route 0)(contents(FileLoaded Coq.Init.Tauto /home/clement/.opam/4.09.0/lib/coq/theories/Init/Tauto.vo))))
(Feedback((doc_id 0)(span_id 1)(route 0)(contents(ProcessingIn master))))
(Feedback((doc_id 0)(span_id 1)(route 0)(contents Processed)))
(Answer query0 Ack)
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(ProcessingIn master))))
(Feedback((doc_id 0)(span_id 1)(route 0)(contents Processed)))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(Message(level Error)(loc(((fname ToplevelInput)(line_nb 1)(bol_pos 0)(line_nb_last 1)(bol_pos_last 0)(bp 15)(ep 16))))(pp(Pp_glue((Pp_string Unable)(Pp_print_break 1 0)(Pp_string to)(Pp_print_break 1 0)(Pp_string locate)(Pp_print_break 1 0)(Pp_string library)(Pp_print_break 1 0)(Pp_string A.))))(str"Unable to locate library A.")))))
(Answer query0(CoqExn((loc(((fname ToplevelInput)(line_nb 1)(bol_pos 0)(line_nb_last 1)(bol_pos_last 0)(bp 15)(ep 16))))(stm_ids((1 2)))(backtrace(Backtrace()))(exn(CErrors.UserError(locate_library"Unable to locate library A.")))(pp(Pp_glue((Pp_glue())(Pp_glue((Pp_glue((Pp_string Unable)(Pp_print_break 1 0)(Pp_string to)(Pp_print_break 1 0)(Pp_string locate)(Pp_print_break 1 0)(Pp_string library)(Pp_print_break 1 0)))(Pp_string A)(Pp_string .)))(Pp_string""))))(str"Unable to locate library A."))))
(Answer query0 Completed)
(Answer EOF Ack)
(Answer EOF Completed)

IOW, coqtop finds libraries in COQPATH but sertop (8.11.0+0.11.0) doesn't. CC @jhagg
@cpitclaudel cpitclaudel mentioned this issue Jul 30, 2020
Closed
@ejgallego ejgallego self-assigned this Aug 26, 2020
@ejgallego ejgallego added this to the 0.12.0 milestone Aug 26, 2020
@ejgallego
Copy link
Collaborator

Same comment that #222

@ejgallego ejgallego modified the milestones: 0.12.0, 0.11.1 Aug 26, 2020
ejgallego added a commit that referenced this issue Aug 26, 2020
@ejgallego
[serapi] Fix #221 "Support COQPATH"
006449d
ejgallego added a commit that referenced this issue Aug 26, 2020
@ejgallego
Merge pull request #224 from ejgallego/v8.11+coqpath
4723859 
[serapi] Fix #221 "Support COQPATH"
ejgallego added a commit to ejgallego/opam-repository that referenced this issue Aug 26, 2020
@ejgallego
[new release] coq-serapi (8.11.0+0.11.1)
b688d42 
CHANGES:

* [general] Require dune >= 2.0 (@ejgallego, ??)
 * [serapi]  New query `Comments` to return all comments in a document
             (@ejgallego, rocq-archive/coq-serapi#20? , (partially) fixes rocq-archive/coq-serapi#191 , ejgallego/coq-serapi#200 )
 * [general] Coq's error recovery is now disabled by default
             (@ejgallego , fixes rocq-archive/coq-serapi#201)
 * [general] New option `--error-recovery` to enable error recovery
             (@ejgallego , rocq-archive/coq-serapi#203)
 * [general] Bump sexplib dependency to v0.13 (@ejgallego , rocq-archive/coq-serapi#204)
             Fixes incorrect change in rocq-archive/coq-serapi#194.
 * [sertop]  Set default value of allow-sprop to be true in agreement with upstream coq v8.11
             and added option '--disallow-sprop' to optionally switch it off
			 (--disallow-sprop forbids using the proof irrelevant SProp sort)
             (rocq-archive/coq-serapi#199, @pestun)
 * [sertop]  Set default value of allow-sprop to be true in agreement with upstream coq v8.11
             and added option '--disallow-sprop' to optionally switch it off
			 (--disallow-sprop forbids using the proof irrelevant SProp sort)
             (@pestun , rocq-archive/coq-serapi#199)
 * [sertop]  Added option `--topfile` to `sertop` to set top name from
             a filename (rocq-archive/coq-serapi#197, @pestun)
 * [deps]    Require sexplib >= 0.12 , fixed deprecation warnings
             (rocq-archive/coq-serapi#194, @ejgallego)
 * [general] SerAPI is now tested with OCaml 4.08 and 4.09 (rocq-archive/coq-serapi#195 , @ejgallego)
 * [sertop ] Forward port sername from 0.7.1 (@ejgallego)
 * [serlib ] Fix rocq-archive/coq-serapi#212 "Segfault on universes" (@ejgallego, reported by @cpitclaudel , rocq-archive/coq-serapi#214)
 * [serapi ] Fix rocq-archive/coq-serapi#221 "Support COQPATH" (@ejgallego, reported by @cpitclaudel , rocq-archive/coq-serapi#224)
 * [sertop ] Fix rocq-archive/coq-serapi#222 "Support --indices-matter" (@ejgallego, reported by @cpitclaudel , rocq-archive/coq-serapi#223)
 * [sertop ] Fix "Stack overflow in main loop" (@pestun , rocq-archive/coq-serapi#216)
@ejgallego ejgallego mentioned this issue Aug 26, 2020
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this issue Aug 27, 2020
@ejgallego
[new release] coq-serapi (8.11.0+0.11.1)
cb00c63 
CHANGES:

* [general] Require dune >= 2.0 (@ejgallego, ??)
 * [serapi]  New query `Comments` to return all comments in a document
             (@ejgallego, rocq-archive/coq-serapi#20? , (partially) fixes rocq-archive/coq-serapi#191 , ejgallego/coq-serapi#200 )
 * [general] Coq's error recovery is now disabled by default
             (@ejgallego , fixes rocq-archive/coq-serapi#201)
 * [general] New option `--error-recovery` to enable error recovery
             (@ejgallego , rocq-archive/coq-serapi#203)
 * [general] Bump sexplib dependency to v0.13 (@ejgallego , rocq-archive/coq-serapi#204)
             Fixes incorrect change in rocq-archive/coq-serapi#194.
 * [sertop]  Set default value of allow-sprop to be true in agreement with upstream coq v8.11
             and added option '--disallow-sprop' to optionally switch it off
			 (--disallow-sprop forbids using the proof irrelevant SProp sort)
             (rocq-archive/coq-serapi#199, @pestun)
 * [sertop]  Set default value of allow-sprop to be true in agreement with upstream coq v8.11
             and added option '--disallow-sprop' to optionally switch it off
			 (--disallow-sprop forbids using the proof irrelevant SProp sort)
             (@pestun , rocq-archive/coq-serapi#199)
 * [sertop]  Added option `--topfile` to `sertop` to set top name from
             a filename (rocq-archive/coq-serapi#197, @pestun)
 * [deps]    Require sexplib >= 0.12 , fixed deprecation warnings
             (rocq-archive/coq-serapi#194, @ejgallego)
 * [general] SerAPI is now tested with OCaml 4.08 and 4.09 (rocq-archive/coq-serapi#195 , @ejgallego)
 * [sertop ] Forward port sername from 0.7.1 (@ejgallego)
 * [serlib ] Fix rocq-archive/coq-serapi#212 "Segfault on universes" (@ejgallego, reported by @cpitclaudel , rocq-archive/coq-serapi#214)
 * [serapi ] Fix rocq-archive/coq-serapi#221 "Support COQPATH" (@ejgallego, reported by @cpitclaudel , rocq-archive/coq-serapi#224)
 * [sertop ] Fix rocq-archive/coq-serapi#222 "Support --indices-matter" (@ejgallego, reported by @cpitclaudel , rocq-archive/coq-serapi#223)
 * [sertop ] Fix "Stack overflow in main loop" (@pestun , rocq-archive/coq-serapi#216)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@ejgallego ejgallego

Labels
kind: bug kind: enhancement
Projects
None yet
Milestone
0.11.1
Development

Successfully merging a pull request may close this issue.

[new release] coq-serapi (8.11.0+0.11.1) ejgallego/opam-repository
2 participants
@ejgallego @cpitclaudel