Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007398OCamltools (ocaml{lex,yacc,dep,debug,...})public2016-11-03 11:472017-04-21 17:42
Reporterkosik 
Assigned To 
PrioritynormalSeverityfeatureReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product Version4.02.3 
Target VersionFixed in Version 
Summary0007398: missing possibility to be able to see "inside" values of abstract types
DescriptionIn Ocaml toplevel as well as in ocamldebug, when I print a value of an abstract type, e.g.:

  Proof_global.give_me_the_proof ();;

what I see is:

  - : Proof.proof = <abstr>

I am not at all against the of abstract types in general, but in specific cases
(when I am exploring an alien codebase I am trying to understand or when I am debugging something) this behavior of ocaml toplevel as well as ocamldebug is not helpful.

There is a possibility to define printers, which is a good option to have for special cases, but in general in many cases the default printers that Ocaml is able to auto-generate could be sufficient. These are not available now.

For example there is no way for me to mark a chosen datatype, at runtime, in the toplevel, as "transparent" and see "inside", like this:

  # Proof_global.give_me_the_proof ();;
  - : Proof.proof =
  {Proof.proofview = <abstr>;
   entry =
    [(Constr.Evar (<abstr>, [||]),
      Constr.Prod (Names.Name.Name "P",
                   Constr.Sort (Sorts.Prop Sorts.Null),
                   Constr.Rel 1))];
   focus_stack = [(<abstr>, <abstr>, <abstr>)]; shelf = [];
   given_up = []; initial_euctx = <abstr>}

To overcome this problem, I need to maintain a special branch with transparent instead of opaque version of types I am interested in. But this is painful and not really professional.

I think it would be very useful to be able to:
- turn transparency/opaqueness of individual data-types on/off.
- (and in some cases maybe even) turn turn on transparency of all data-types.

I think, this would make Ocaml more pleasant to work with.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0016504)
shinwell (developer)
2016-11-03 16:03

The forthcoming gdb support automatically sees through abstract types, so this should help.
(0016553)
xleroy (administrator)
2016-11-11 20:11

The recommended workaround is to export a printing function for your abstract type and install it as a printer in the toplevel or in ocamldebug. It works very well for the toplevel, not so well for ocamldebug.

I don't know if any of the gdb support for opaque types that shinwell mentions could find its way back into ocamldebug. Probably not any time soon.

I move to "resolve/suspended" this PR, as there is no resolution in sight.
(0017746)
kosik (reporter)
2017-04-21 11:00

We are aware of the workaround. We are just reporting that it is *not feasible* and a *bad idea* to use it in case we are dealing with more than one or two datatype (think of Coq).

Writing pretty-printers for abstract data types is an expensive, annoying, tedious, futile and retarded activity.
(0017747)
kosik (reporter)
2017-04-21 11:22

E.g. if I want to see what is going on, at the moment, I must turn abstract data-types to concrete ones:

https://github.com/matejkosik/coq/commits/trunk__transparent [^]

Then, I get the pretty-printers for free, which is great.

It would be tremendous, if this kind of uncivilized workaround wasn't necessary.
(0017748)
gasche (developer)
2017-04-21 14:03

Emilio uses ppx_deriving in his SerApi project, the same approach could be used to derive pretty-printers.
(0017749)
kosik (reporter)
2017-04-21 14:08

I've asked Emilio about this aspect.

His answer was (IIUC) is that in case of abstract data-types, he does not see anything either.

How could he?
(0017752)
ejgallego (reporter)
2017-04-21 17:42

Indeed, as SerAPI builds _on top_ of Coq, we can only see types that are public, this is sometimes a pain.

The medium term plan is to enable Coq to have a proper CRUD interface for types, etc... but that requires adding external dependencies and it is a pain.

I have some experimental overlays on SerAPI that ship their own definition and use Obj.magic to expose private types. This works, but it is very dangerous.

- Issue History
Date Modified Username Field Change
2016-11-03 11:47 kosik New Issue
2016-11-03 16:03 shinwell Note Added: 0016504
2016-11-11 20:11 xleroy Note Added: 0016553
2016-11-11 20:11 xleroy Status new => acknowledged
2016-12-07 16:37 doligez Category OCaml tools (ocaml{lex,yacc,dep,browser,debug}) => OCaml tools (ocaml{lex,yacc,dep,debug})
2017-02-23 16:45 doligez Category OCaml tools (ocaml{lex,yacc,dep,debug}) => tools (ocaml{lex,yacc,dep,debug,...})
2017-04-21 11:00 kosik Note Added: 0017746
2017-04-21 11:22 kosik Note Added: 0017747
2017-04-21 14:03 gasche Note Added: 0017748
2017-04-21 14:08 kosik Note Added: 0017749
2017-04-21 17:42 ejgallego Note Added: 0017752


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker