coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Debugging plugins with ocamldebug in Emacs

From: Tj Barclay <tjbarclay AT ku.edu>
To: <coq-club AT inria.fr>
Subject: [Coq-Club] Debugging plugins with ocamldebug in Emacs
Date: Tue, 8 Jun 2021 13:29:09 -0500
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass (sender ip is 129.237.34.11) smtp.rcpttodomain=inria.fr smtp.mailfrom=ku.edu; dmarc=bestguesspass action=none header.from=ku.edu; dkim=none (message not signed); arc=none
Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=4zQSgBT8d7Gg+o0bSMd+YUe8NA2rhXQTr8EMGNM+us4=; b=YlDTPmN19/eSSjR4+6Yvn0zxjufP2SnqAMz7+h99qyZ63UWS4S0IQK8J73ZvgdHc6odnwSGdfOop8r5lEiPO7S0QllvD6oB8FvusOD7a5clWsk/c+06wo0zWA7342K93phDq8LgJrX+jUBE0JSIgmwJ9Gyn4HJWCchSGPShrWBrzbA4S3nWVugWI+9pq03a7xpVcvkIesYEdlT5vMVnDSQ0qEcpj/DzxlRzfVGjFgB6HH4wged7zDOKV4tJ5BpqSv4i/LHnhG9R/h2xNgzVaKkMrSq2CYC3bo1hEI3pLDjNb6x4S6k5Sj7atnENn4e2cuH1SyfKhR6KuUCYGRxjgMg==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=GI6xgQ7BAdb1teiN2X6qmrQK79QIbmd4F3638Dn8nl7KG61e7ugXCTXYacdHyjLGizuHs8FjDdzIrBJNsuNpnuXXrevssGRmQnWFCvujfrgynRrxPAxSnArsomljNhaS8odl8n6LlaqbMy/1g+CI2b/N2+rguRUWgE4kfL6QrQ973fuTC4ShNTyFMRwS0Re6YnIesYm7YZE7++nOaVKba74RiX72n6vd7m3N8U1QQrfXyyYXB5EBmVORIhNmasXGeNf2XaWmbrYQNtgM6BRACXsMiNfVurM2ghdo2cAj/tPQE0sZAFej1G0DviR2j3wN9XcO99aU0um4cOmlpW2HNA==
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tjbarclay AT ku.edu; spf=Pass smtp.mailfrom=tjbarclay AT ku.edu; spf=Pass smtp.helo=postmaster AT NAM04-BN8-obe.outbound.protection.outlook.com
Ironport-hdrordr: A9a23:gPt/u6HKPWL6uZEdpLqFmZHXdLJyesId70hD6qkXc20vTiX4rbHXoB1/73TJYVkqKQsdcK+7Sdy9qB/nhPpICMwqXYtKPjOWxFdAXbsSlLcKqgeIc1yNygce79YCT0EUMqyXMbEVt7ec3CCIV/cJ+p2uzZ2Br8a29RhQpHlRGt9dBlBCazpzaXcGOTVuNN4ALN622vBmgBabQzAwVeSUJl5tZYb+juyOrKqjTjIvOnccgjWmvHeR0PrfMzy1ty1uLA9n8PMbySzgmwz96r7LiYDL9jbsk1fqq69bgd7w69NYBaW3+7goAwSpsj7tXqhHdoejjxxdmpDd1H8a1OH15y0bEK1Ihk/5TyWMmV/W5jnE/F8Vmh3f4G7duUOmkOjQZBcbLOVm7Lg0TjLpr3IZ+NV93ctwrgeki6Y=
Ironport-phdr: A9a23:0+imXBAIhmw9bvBxyA3GUyQU1EMY04WdBeb1wqQuh78GSKm/5ZOqZBWZuaw8ygSRDM6LsbptsKn/i+jYQ2sO4JKM4jgpUadncFs7s/gQhBEqG8WfCEf2f7bAZi0+G9leBhc+pynoeUdaF9zjaFLMv3a88SAdGgnlNQpyO+/5BpPeg9642uyv/5DfeQtFiCa5bL99Lxi6sxjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjE28G/ZhM9+gr9Frh29phxy2JTbbJ2POfdkYq/RYdEXSGxcVchRTSxBBYa8YpMRAeoDIO1VspPyp0ESohu6HwatBP7kxzhUhn/0xqI1yf4hHh3C3AM6H9MDq3fUrMjvOKgMTO+10bDFwDPeZPxZxTnz8pLHcgw9of6SR7Jwd9LcxE0xGg7Kk1mdq4/oMTOa2OkJrWWW8uRtWP6vhWM5pQx8rSWiy8csh4TKiIwbyk3I+yV6zYg7J9C0VkF1bNG6HJZWqiqUOYx2QsY4TGFpviY30qEJuZmifCgWz5Qn3wTTa/mDc4SQ/h3jU/+RITN/hHJiYLKznROy8Uymx+bhVce0yE5HoyVZntXWq3wByx7e5tKaRvdh4kutwyuD2x7P5u1cPEw4i67WJ4Q/zrM+lJcfq1nPEyDslEnriKKbcFgv9PKy5OT9eLrmo4eRN49qhQH6NaQjgtSxDPg/PAQSUGWX4Pmx2qXg8EHgR7VFleM5nrPesJDHOcQUvam5AxJT0ok+8Rq/Fy2m0NMEnXYZMF1FZBOHj4/vO13UJ/D4EOu/g1CrkDdsxPDKJKHuApLILnTbkbfhe6hy61JExQc80dxT/Y9YBq0DLf7pR0P9qMDUAgUkPwCq3+rrENB92ZkfWWKLDK+ZKqTSsVqQ6+IzIemDf5UauCzhJPgh/fHvjWQ0mVwAfaWzw5QYdW24Eux8I0qFeXrsnssBEWASswUiS+zqkUSOXiJXZ3avRK0x/So7CYKjDYfbXI+hmr2B3CGhHp1XfG9KEF6MEW27P7mDDqMHbzvXKct8mBQFU6KgQskvz0f9mhX9zu9bLKL+8zcTsZvynIxp5efajxo2/C1cDNnb3m2QGTIn1lgUTiM7ifgs6Xd2zU2OhPAQaxlwFsEV6v9UAF9S3X/06cVfU4y3cCSRO9CDRRChX8msBiw3QpQp2dgSbk1hGtKkyBfewy6tBLxTnLuOVsVcGk303GW3KspgmS+u6Q==

Howdy,

I've been trying to figure out how to debug the extraction plugin. What I'd like to do is execute an Extraction vernacular command in coqtop (or PG if that's an option) and have that go until hitting a breakpoint set in one of the plugin's .ml files. So far all I've managed to get working is running coqtop in ocamldebug using the provided code in dev/tools/coqdev.el. From there I can set breakpoints in files like toplevel/coqtop.ml and toplevel/coqloop.ml, but can't set breakpoints in plugins/extraction/*.ml even after Require Extraction.

I appreciate any tips on how to get this going, or guidance on how to properly go about debugging Coq plugins in general if what I'm proposing doesn't work or isn't recommended.

Best,

TJ Barclay

Electrcial Engineering & Computer Science, University of Kansas

tjbarclay AT ku.edu

+1 316 259 2250

[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