TVL depot development (mail to depot@tvl.su)
 help / color / mirror / code / Atom feed
From: sternenseemann <sternenseemann@systemli•org>
To: depot@tvl.su
Subject: [tvix] Value Location, Value Documentation
Date: Fri, 2 Jun 2023 23:49:16 +0200	[thread overview]
Message-ID: <5d2a7439-2a0a-791b-7b36-668427e296ef@systemli.org> (raw)

Hi all,

I want to feel you out on a specific issue that is mostly a question of 
//tvix/eval, but still far-ish away.

Currently we can relate specific VM instructions back to a source 
location that caused them to be emitted by the compiler. This seems to 
work well enough for traces stemming from runtime errors.

We may also need to or want to relate values back to source locations in 
the following ways:

* builtins.unsafeGetAttrPos demands that we are able to return the
   source location where an attribute (given by its name) of a specific
   attribute set (given as a value) is defined. Note that the location
   where the attribute and its attribute value were defined may differ,
   e.g.:

     let val = 42; set = { attrName = val; }; in
     builtins.unsafeGetAttrPos "attrName" set

   val itself would trace back to a different location compared to the
   unsafeGetAttrPos expression.

* Additionally, I have the inclination that it would be useful to be
   able to retrieve the definition location of arbitrary values at
   runtime, but this is currently not strictly required.

   This feature would not (need to) be exposed in the language via a
   builtin, but instead used in the following ways:

   1. To enhance runtime traces. Similarly to how C++ Nix is able to
      display the source locations of lambdas during evaluation.

   2. To retrieve documentation: This would then work similarly to
      what Robert Hensing proposed for C++ Nix: The already tracked
      value location would be used to extract the documentation
      comment associated with it from the still available source
      file. This has the advantage that it has no runtime overhead
      unless used (assuming you are already tracking value source
      locations). See <https://github.com/NixOS/nix/pull/1652>.
      Robert's PR has become stale since, but would become relevant
      again if RFC0145 (<https://github.com/NixOS/rfcs/pull/145>)
      succeeds.

      An alternative was proposed by Eelco to support documentation
      via an extra attribute in a functor, but I don't think too
      many like this solution (<https://github.com/NixOS/nix/pull/5527>).
      andi- floated the idea of having a builtin to attach documentation
      to values in the same thread 
(<https://github.com/NixOS/nix/pull/5527#issuecomment-967236780>).
      Both ideas have the disadvantage that they cause runtime overhead
      even if the documentation is not used. Additionally, they make it
      hard to impossible to statically generate documentation à la
      nixdoc.

      hsjobeki has proposed a CL (<https://cl.tvl.fyi/8530>) for Tvix
      that implements a weird mix of both approaches: Documentation
      comments' contents are attached to lambda values (and lambda
      values only) at compile time, so that they can be retrieved
      at runtime (e.g. via the repl). This of course incurs an
      increased memory overhead regardless of whether the documentation
      is used or not.

Given this outline, I'd be interested to know:

- How can we implement source location tracking of values? How far are
   we willing/able to go (i.e. do we want to limit ourselves to
   unsafeGetAttrPos)?

- Or more explicitly: Do we want to stay away from mapping values to
   source locations as much as possible, as it is an inherently
   treacherous business in Nix?

- How do we want documentation to work? What are our requirements? This
   is especially interesting for RFC0145—as I am one of the shepherds,
   I can provisionally enter Tvix's perspective into the discussion.

-sterni

             reply	other threads:[~2023-06-02 21:49 UTC|newest]

Thread overview: 2+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2023-06-02 21:49 sternenseemann [this message]
2023-07-03  9:36 ` Adam Joseph

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=5d2a7439-2a0a-791b-7b36-668427e296ef@systemli.org \
    --to=sternenseemann@systemli$(echo .)org \
    --cc=depot@tvl.su \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html
Be sure your reply has a Subject: header at the top and a blank line before the message body.
Code repositories for project(s) associated with this public inbox

	https://code.tvl.fyi

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).