Romain Tetley (Apr 26 2024 at 13:02): Romain Tetley (Apr 26 2024 at 13:02):anyways thanks for your answers, I think I got the info I wanted !
Notification Bot (Apr 26 2024 at 13:02):Romain Tetley has marked this topic as resolved.
Gaëtan Gilbert (Apr 26 2024 at 13:13):I mean in the code we literally write hov 2 (pr_constr c), if c is eg Set then pr_constr c is str "Set" and if c is f x then pr_constr c is str "f" ++ spc() ++ str "x"
and hov is defined as let hov n s = Ppcmd_box(Pp_hovbox n,s)
Romain Tetley (Apr 26 2024 at 13:13):Gaëtan Gilbert said:
I mean in the code we literally write
hov 2 (pr_constr c), ifcis egSetthenpr_constr cisstr "Set"and ifcisf xthenpr_constr cisstr "f" ++ spc() ++ str "x"
andhovis defined aslet hov n s = Ppcmd_box(Pp_hovbox n,s)
Yeah I understand !
Emilio Jesús Gallego Arias (Apr 26 2024 at 13:21):Why not to use Shachar's existing translator?
Romain Tetley (Apr 26 2024 at 13:32):I'm not sure what you are referring to ? Could you give me some pointers ?
Emilio Jesús Gallego Arias (Apr 26 2024 at 14:15):I am talking about option 1 here https://coq.zulipchat.com/#narrow/stream/237662-VsCoq-devs-.26-users/topic/what.20happened.20to.20vscoq.20formatting.20in.20visual.20studio/near/426147047
Romain Tetley (Apr 26 2024 at 14:16):Yes I understand this ! Would you mind sending a pointer to the code ? Thanks for your help !
Emilio Jesús Gallego Arias (Apr 26 2024 at 14:19):We are hosting two similar copies now:
Note my comment in that thread:
IMHO the UI roadmap for Coq really needs a very urgent discussion, but for this issue in particular I'd approach it first by porting Shachar's printer to React, finish Shachar test suite, and maybe package it if you want in
npm.
Romain Tetley (Apr 26 2024 at 14:21):Yes I agree with you !
Romain Tetley (Apr 26 2024 at 14:21):Regarding that library it's not really helpful in effect because you don't seem to support hov boxes which is what I am trying to support
Romain Tetley (Apr 26 2024 at 14:21):At least from a quick glance ?
Romain Tetley (Apr 26 2024 at 14:22):I'll have to look at it some more
Emilio Jesús Gallego Arias (Apr 26 2024 at 14:22):As far as I know it does support it
Emilio Jesús Gallego Arias (Apr 26 2024 at 14:22):But @Shachar Itzhaky is the authority on it
Romain Tetley (Apr 26 2024 at 14:23):well there is a comment saying /** @todo hov mode */
Romain Tetley (Apr 26 2024 at 14:23):and no reference to other modes then vertical and horizontal
Romain Tetley (Apr 26 2024 at 14:23):but I'll read the code to make sure !
Romain Tetley (Apr 26 2024 at 14:24):This in particular makes me doubt you support it:
// ["Pp_box", ["Pp_vbox"/"Pp_hvbox"/"Pp_hovbox", _], content]
case "Pp_box":
let [bty, offset] = pp[1],
mode = bty == "Pp_vbox" ? "vertical" : "horizontal";
return this.makeBox(this.pp2DOM(pp[2]), mode, bty, offset);
but you do pass it bty so maybe I'm wrong ?
Emilio Jesús Gallego Arias (Apr 26 2024 at 14:26):There are handled as h boxes yes, but I don't know enough of Format internals as to understand how bad is this in practice. I understand the current setting was enough for Software Foundations
Shachar Itzhaky (May 22 2024 at 13:42):@Romain Tetley did you test this? we would appreciate some insights
Romain Tetley (May 22 2024 at 14:23):I did ! It seems you actually do handle hov_box to an extent with some css tricks
Jim Fehrle (May 24 2024 at 22:45):@Romain Tetley Did you ever consider linking binary code from the OCaml Pp.t to format it in vsCoq2? Just a stray thought. Sounds like you're already working on a different approach.
Romain Tetley (May 28 2024 at 07:12):I did consider an adjacent approach, but in the end yes I'm working on another solution
Last updated: Oct 13 2024 at 01:02 UTC