coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] "undefined symbol: camlTacarg" with Coq trunk?

From: e AT x80.org (Emilio Jesús Gallego Arias)
To: Jason Gross <jasongross9 AT gmail.com>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] "undefined symbol: camlTacarg" with Coq trunk?
Date: Wed, 29 Mar 2017 10:52:33 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Neutral smtp.mailfrom=e AT x80.org; spf=None smtp.helo=postmaster AT cc-tupan-roaming-a.ensmp.fr
Ironport-phdr: 9a23:pcDoeRF2KZK3qPF/VGG3LZ1GYnF86YWxBRYc798ds5kLTJ7zpc2wAkXT6L1XgUPTWs2DsrQf2raQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbQhFgDWwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VC+85Kl3VhDnlCYHNyY48G7JjMxwkLlbqw+lqxBm3oLYfJ2ZOP94c6jAf90VWHBBU95RWSJfH428aIUPAeQDMuhboYbyqEcBoACiBQWwHu7j1iNEi2X00KA8zu8vERvG3AslH98WrnvZt9r0OaQOXeyvy6nI1zrDZO5S1Tny7YjIcxQhofCLXbltdcTe11IvDxnejl6NqILqJTeV1uATvGiU6OprSP6ii3Qmqw5ruTijw8EhgZTHiIISz1DL7yR5wIAtKN23SU57fd6kEIZLuC2AK4R2RcYiTmd1syg50r0LoYO3cSwFxZg92RLTdvOKf5KV7h/jV+udOyp0iXxndb6ngxu+71Ksx+ngWsWuzlpGsjBJn93Nu30Lyhfd8NKISuFn8UekwTuP1x7c6uVDIU0siaXUN4ctwqItlpoLq0vDGDb6mF/xjKCMc0Uk++6o6+v+brr8vJOTKYl0ihr7MqQ2gMC/D/44PhAPX2id5+u8yKXu8VD9TbhFlPE6jLTVvZ/AKcgGpqO0ABVZ3pst5hu9Fzum1c4XnXgDLFJLYhKHiI3pNknQL/3jAvaygEignC1sx/DcMb3tGo/NIWTbkLf9YbZ97FZRxxY0zdBG/p5bFrUBIO/oVULqr9zZDho5MxSuzOr9CdV90JkeWWOVDaODPqPSqwzA2uV6AeCXY4ldlyz6MONts/znlng/lkUaZrL49ZQSYXG8WP9hJhPKT2Drh4IMOXda5kw5VuOiyHCHUDpSYD6QUrmu/XkUAYaiAIjEDqm3gbWanXToVqZKb3xLXwjfWUzjcJ+JDrJVMHqf
Organization: X80 Heavy Industries

Hi Jason,

Jason Gross
<jasongross9 AT gmail.com>
writes:

> When I try to build Bedrock (`make src`, branch 8.4+8.5,
> https://github.com/JasonGross/bedrock/tree/8.4%2B8.5) with Coq trunk, I get
>
> COQC Bedrock/ILTac.v
> Warning: Unknown warning name: deprecated-appcontext
> [unknown-warning,toplevel]
> File "./Bedrock/ILTac.v", line 17, characters 0-25:
> Error:
> while loading
> /scratch/var/lib/jenkins/workspace/bedrock-src-trunk/coq_version/trunk/Bedrock/reification/reif.cmxs:
> error loading shared library:
> /scratch/var/lib/jenkins/workspace/bedrock-src-trunk/coq_version/trunk/Bedrock/reification/reif.cmxs:
> undefined symbol: camlTacarg

Did you do `open Ltac_plugin` in reif.ml, as instructed in
`dev/doc/changes.txt` ?

E.

[Coq-Club] "undefined symbol: camlTacarg" with Coq trunk?, Jason Gross, 03/29/2017
- Re: [Coq-Club] "undefined symbol: camlTacarg" with Coq trunk?, Emilio Jesús Gallego Arias, 03/29/2017
  - Re: [Coq-Club] "undefined symbol: camlTacarg" with Coq trunk?, Emilio Jesús Gallego Arias, 03/29/2017
    - Re: [Coq-Club] "undefined symbol: camlTacarg" with Coq trunk?, Jason Gross, 03/29/2017