tlaplus / tlapm

The TLA Proof Manager
https://proofs.tlapl.us/
BSD 2-Clause "Simplified" License
65 stars 20 forks source link

Emit bytecode in dune build for debugging #144

Closed ahelwer closed 1 month ago

ahelwer commented 2 months ago

This will generate a tlapm.bc OCaml bytecode file in _build/default/src which can be loaded by ocamldebug. Dune 2.0+ requires this to be explicitly specified (docs):

Given an executable stanza with (name \<name>), Dune will know how to build \<name>.exe. If requested, it will also know how to build \<name>.bc and \<name>.bc.js (Dune 2.0 and up also need specific configuration (see the modes optional field below)).

ocamldebug also requires everything to be built with the -g flag, which is the case by default with Dune; see output of dune printenv ..

Ref https://github.com/tlaplus/tlapm/discussions/143

I also added a debug launch profile for VS Code, and added the earlybird DAP server to the opam-deps-dev make target.

ahelwer commented 2 months ago

It should be noted that the generated tlapm.bc is very large:

>ls -lh tlapm.*
-r-xr-xr-x 1 ahelwer ahelwer  22M Jul 14 18:30 tlapm.bc
-r-xr-xr-x 1 ahelwer ahelwer 5.1M Jul 14 18:30 tlapm.exe
-r--r--r-- 1 ahelwer ahelwer  178 Jul 14 17:55 tlapm.ml
-r--r--r-- 1 ahelwer ahelwer  139 Jul 14 17:55 tlapm.mli

So perhaps these changes must be paired with logic to avoid bundling it into the zip file. Although looking at the make release target perhaps this is not actually an issue and the .bc file will not be included.

ahelwer commented 1 month ago

@kape1395 what do you think of these changes?

ahelwer commented 1 month ago

@kape1395 actually I think these changes should be reverted, because after a few weeks playing around with the OCaml debugger I have found it is just too immature to use as a development tool and the utop REPL should be used instead. This seems to be the general idea in the OCaml community as well.

kape1395 commented 1 month ago

@ahelwer, I would like to keep the changes. Even if they are not that useful today, they don't harm anyone either.

ahelwer commented 1 month ago

All right, although in order to be able to actually set breakpoints (in some places) you need this dune parameter set to false (it's true by default), and I don't know whether we want that: https://dune.readthedocs.io/en/stable/reference/dune-project/map_workspace_root.html