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

Strange output when using debug printers (source db) #8952

Closed
SkySkimmer opened this issue Nov 9, 2018 · 3 comments
Closed

Strange output when using debug printers (source db) #8952

SkySkimmer opened this issue Nov 9, 2018 · 3 comments
Labels
kind: user messages Error messages, warnings, etc.

Comments

@SkySkimmer
Copy link
Contributor 

$ dev/ocamldebug-coq bin/coqtop.byte -compile /tmp/foo.v
        OCaml Debugger version 4.07.1

(ocd) source db
File /home/gaetan/.opam/4.07.1/lib/ocaml/threads/threads.cma loaded
File /home/gaetan/.opam/4.07.1/lib/ocaml/str.cma loaded
File /home/gaetan/.opam/4.07.1/lib/camlp5/gramlib.cma loaded
File /home/gaetan/dev/coq/coq/config/config.cma loaded
File /home/gaetan/dev/coq/coq/clib/clib.cma loaded
File /home/gaetan/.opam/4.07.1/lib/ocaml/dynlink.cma loaded
File /home/gaetan/dev/coq/coq/lib/lib.cma loaded
File /home/gaetan/dev/coq/coq/kernel/kernel.cma loaded
File /home/gaetan/dev/coq/coq/library/library.cma loaded
File /home/gaetan/dev/coq/coq/engine/engine.cma loaded
File /home/gaetan/dev/coq/coq/pretyping/pretyping.cma loaded
File /home/gaetan/dev/coq/coq/interp/interp.cma loaded
File /home/gaetan/dev/coq/coq/proofs/proofs.cma loaded
File /home/gaetan/dev/coq/coq/parsing/parsing.cma loaded
File /home/gaetan/dev/coq/coq/printing/printing.cma loaded
File /home/gaetan/dev/coq/coq/tactics/tactics.cma loaded
File /home/gaetan/dev/coq/coq/vernac/vernac.cma loaded
File /home/gaetan/dev/coq/coq/stm/stm.cma loaded
File /home/gaetan/dev/coq/coq/toplevel/toplevel.cma loaded
File /home/gaetan/.opam/4.07.1/lib/ocaml/threads/threads.cma loaded
File /home/gaetan/.opam/4.07.1/lib/ocaml/str.cma loaded
File /home/gaetan/.opam/4.07.1/lib/camlp5/gramlib.cma loaded
File /home/gaetan/dev/coq/coq/config/config.cma loaded
File /home/gaetan/dev/coq/coq/clib/clib.cma loaded
File /home/gaetan/.opam/4.07.1/lib/ocaml/dynlink.cma loaded
File /home/gaetan/dev/coq/coq/lib/lib.cma loaded
already open 
File /home/gaetan/dev/coq/coq/kernel/kernel.cma loaded
File /home/gaetan/dev/coq/coq/library/library.cma loaded
File /home/gaetan/dev/coq/coq/engine/engine.cma loaded
File /home/gaetan/dev/coq/coq/pretyping/pretyping.cma loaded
File /home/gaetan/dev/coq/coq/interp/interp.cma loaded
File /home/gaetan/dev/coq/coq/proofs/proofs.cma loaded
File /home/gaetan/dev/coq/coq/parsing/parsing.cma loaded
File /home/gaetan/dev/coq/coq/printing/printing.cma loaded
File /home/gaetan/dev/coq/coq/tactics/tactics.cma loaded
File /home/gaetan/dev/coq/coq/vernac/vernac.cma loaded
File /home/gaetan/dev/coq/coq/stm/stm.cma loaded
File /home/gaetan/dev/coq/coq/toplevel/toplevel.cma loaded
File /home/gaetan/dev/coq/coq/plugins/ltac/ltac_plugin.cmo loaded
File /home/gaetan/dev/coq/coq/dev/top_printers.cmo loaded
(ocd)

but if I paste the contents of db instead:

dev/ocamldebug-coq bin/coqtop.byte -compile /tmp/foo.v
        OCaml Debugger version 4.07.1

(ocd) source core.dbg
File /home/gaetan/.opam/4.07.1/lib/ocaml/threads/threads.cma loaded
File /home/gaetan/.opam/4.07.1/lib/ocaml/str.cma loaded
File /home/gaetan/.opam/4.07.1/lib/camlp5/gramlib.cma loaded
File /home/gaetan/dev/coq/coq/config/config.cma loaded
File /home/gaetan/dev/coq/coq/clib/clib.cma loaded
File /home/gaetan/.opam/4.07.1/lib/ocaml/dynlink.cma loaded
File /home/gaetan/dev/coq/coq/lib/lib.cma loaded
File /home/gaetan/dev/coq/coq/kernel/kernel.cma loaded
File /home/gaetan/dev/coq/coq/library/library.cma loaded
File /home/gaetan/dev/coq/coq/engine/engine.cma loaded
File /home/gaetan/dev/coq/coq/pretyping/pretyping.cma loaded
File /home/gaetan/dev/coq/coq/interp/interp.cma loaded
File /home/gaetan/dev/coq/coq/proofs/proofs.cma loaded
File /home/gaetan/dev/coq/coq/parsing/parsing.cma loaded
File /home/gaetan/dev/coq/coq/printing/printing.cma loaded
File /home/gaetan/dev/coq/coq/tactics/tactics.cma loaded
File /home/gaetan/dev/coq/coq/vernac/vernac.cma loaded
File /home/gaetan/dev/coq/coq/stm/stm.cma loaded
File /home/gaetan/dev/coq/coq/toplevel/toplevel.cma loaded
(ocd) load_printer ltac_plugin.cmo
File /home/gaetan/dev/coq/coq/plugins/ltac/ltac_plugin.cmo loaded
(ocd) load_printer top_printers.cmo
File /home/gaetan/dev/coq/coq/dev/top_printers.cmo loaded
(ocd) source top_printers.dbg
(ocd)

Why is source db loading stuff twice?
@SkySkimmer SkySkimmer added the kind: user messages Error messages, warnings, etc. label Nov 9, 2018
@SkySkimmer SkySkimmer mentioned this issue Jan 16, 2020
Closed
@ppedrot
Copy link
Member

ppedrot commented Jan 16, 2020

Reading the source code of the debugger, it seems that the source command is not reentrant. This is probably wreaking havoc when calling source inside a source command.

@ejgallego ejgallego mentioned this issue Jan 20, 2020
Merged
@ejgallego
Copy link
Member

ejgallego commented Jan 20, 2020 •
edited
Loading

Maybe this is worth reporting upstream as Gaëtan has noted.

@SkySkimmer SkySkimmer mentioned this issue Jan 27, 2020
Closed
@SkySkimmer
Copy link
Contributor Author

Reported ocaml/ocaml#9265

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: user messages Error messages, warnings, etc.
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@ppedrot @SkySkimmer @ejgallego