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.

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

missing possibility to be able to see "inside" values of abstract types #7398

Closed
vicuna opened this issue Nov 3, 2016 · 9 comments
Closed

Comments

@vicuna
Copy link

vicuna commented Nov 3, 2016

Original bug ID: 7398
Reporter: kosik
Status: acknowledged (set by @xavierleroy on 2016-11-11T19:11:51Z)
Resolution: open
Priority: normal
Severity: feature
Version: 4.02.3
Category: tools (ocaml{lex,yacc,dep,debug,...})
Monitored by: @gasche @ygrek

Bug description

In 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.

@vicuna
Copy link
Author

vicuna commented Nov 3, 2016

Comment author: @mshinwell

The forthcoming gdb support automatically sees through abstract types, so this should help.

@vicuna
Copy link
Author

vicuna commented Nov 11, 2016

Comment author: @xavierleroy

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.

@vicuna
Copy link
Author

vicuna commented Apr 21, 2017

Comment author: kosik

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.

@vicuna
Copy link
Author

vicuna commented Apr 21, 2017

Comment author: kosik

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.

@vicuna
Copy link
Author

vicuna commented Apr 21, 2017

Comment author: @gasche

Emilio uses ppx_deriving in his SerApi project, the same approach could be used to derive pretty-printers.

@vicuna
Copy link
Author

vicuna commented Apr 21, 2017

Comment author: kosik

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?

@vicuna
Copy link
Author

vicuna commented Apr 21, 2017

Comment author: @ejgallego

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.

@vicuna vicuna added the tools label Mar 14, 2019
@ejgallego
Copy link

I am not sure what should be done with this issue; likely closed.

As @xavierleroy pointed out, the standard solution is to generate a printer [using PPX if you want] and have it installed; thanks to recent tooling improvements this process has been much streamlined and IMO discussion should happen in the corresponding issues (i.e.: ocaml-community/utop#269 )

I have been working on a prototype ppx that indeed uses Obj.magic to enforce transparency of types for serialization purposes; while annoying, I find this approach very practical as it allows you to layer serializers as an extra dep.

@gasche
Copy link
Member

gasche commented Mar 15, 2019

Yep, closing for now as there are no plans to change things in the core-language side. The topic of serialization is of course interesting and worth discussing in the community -- feel free to comment more here if pertinent.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

3 participants