coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Debugging plugins with ocamldebug in Emacs

From: Jim Fehrle <jim.fehrle AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Debugging plugins with ocamldebug in Emacs
Date: Tue, 8 Jun 2021 12:20:54 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jim.fehrle AT gmail.com; spf=Pass smtp.mailfrom=jim.fehrle AT gmail.com; spf=None smtp.helo=postmaster AT mail-il1-f176.google.com
Ironport-hdrordr: A9a23:nfjI+K6G14tpwTwYZQPXwPHXdLJyesId70hD6qkRc20tTiX8raqTdZsgpHrJYVoqKRMdcJW7Scq9qBDnlKKdg7NhWYtKNTOO0ACVxcNZjbcKqAeQfBEWmNQts5uIsJITNDQzNzVHZArBjzVQ2uxP/OW6
Ironport-phdr: A9a23:XNuRMRxBI6FsLm7XCzLgylBlVkEcU1XcAAcZ59Idhq5Udez7ptK+ZR2Zvq08xw+TFazgqNt8w9LMtK7hXWFSqb2gi1slNKJ2ahkelM8NlBYhCsPWQWfyLfrtcjBoVJ8aDAwt8H60K1VaF9jjbFPOvHKy8SQSGhLiPgZpO+j5AIHfg9mz2uyo9ZDffwFFiDW+bL9sMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhygJNzE78G/ZhM9+gr9Frh29vBFw2ZLYbZuPOfZiYq/Qf9UXTndBUMZLUCxBB5uxYY8OD+oEIO1Wr5fyp1sUrRu6GwanGeTiyj1Jhn/zx6E63fouEQHc3AwkAd0Dq3vUrNDvO6cTVeC51rXHzTLGb/5P3zr29YfHfAw7r/6WQbJwbdTeyVMpFw7dklidqpLoMjea2+kMt2WW7fZsWPyhhWMjtw18vjyiytsth4THh48Y1E7J+Tl9zYsxJ9C1R0B1bMOrHpZNqSyWK417Sd4hTWFwoCs21KEKtJqhcCUJyJkr3QPTZv2GfoSS/x7uVuecLDFlj3x/Yr2/nQy98U24x+38SMa01FFKozJAktbWt3AN0wXf6smDSvdg50uh1yuD2gLS5+1eLkA0kq3bK5ElwrEujJYcrUPDHirulEX3iq+ZaFkk9/C25+j7ZrjqvJyROo9uhg3jM6kjm9azDfk6PwUPR2Sb/P6z1Lzn/U33WrVKifg2n7HbsJDbIMQXvKC5DBFV0oY57xawESyr0NsdnXYdLVJFfAiLgJTuO1HLOPz4F+uwg0ywkDd3wPDLJqHuApLULnTajLjheat95FVHxQoozdFf4opUBasbLPLyXE/xrt3YAQUjPwy62ea0QOl6g4gZQCeEBrKTGKLUq16BoOw1cMeWY4pAmjf4Y9Yo5+TqgDdtm14YO6ek3YETZVi3G/1nJwOSZn+60YRJKnsDogdrFL+is1aFSzMGPx5auooz4zg6DMStCoKRHuhFb5SO2S66GttdYWUUUzhk8F/tfoSAHvYIMWece5A/1DMDUrelRskq0hT87GfH

I tried using ocamldebug a couple years ago and found it was not too helpful because it's so limited. I rely on adding print statements instead.

Note that OCaml stack traces omit frames for routines that call another routine as their final statement (a tail recursion optimization). Function names were not shown in the trace (only filename and offset), though I think that was changed recently.

Jim

[Coq-Club] Debugging plugins with ocamldebug in Emacs, Tj Barclay, 06/08/2021
- Re: [Coq-Club] Debugging plugins with ocamldebug in Emacs, Gaëtan Gilbert, 06/08/2021
  - Re: [Coq-Club] Debugging plugins with ocamldebug in Emacs, Jim Fehrle, 06/08/2021
    - Re: [Coq-Club] Debugging plugins with ocamldebug in Emacs, Pierre Courtieu, 06/09/2021