coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Makefile targets

From: "N. Raghavendra" <nyraghu27132 AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Makefile targets
Date: Sat, 16 Dec 2017 00:11:30 +0530
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=nyraghu27132 AT gmail.com; spf=Pass smtp.mailfrom=nyraghu27132 AT gmail.com; spf=None smtp.helo=postmaster AT mail-pf0-f177.google.com
Ironport-phdr: 9a23:v2hI+RQgCfOw5BT6dlbaOEgRONpsv+yvbD5Q0YIujvd0So/mwa6yYxON2/xhgRfzUJnB7Loc0qyK6/mmATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfa5+IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/mHJhMJtjq1brhyupwZxzYDXb46aKPVwc7jBfdMDX2dNQtpdWjZDD466coABD/ABPeFdr4TlqVcAtQGyDhSwCuz1xT9IhmX53bMk3OQnDA7GxhYvE9wTu3nTqtX0NL0SXvq6zKnI0DXPcfFb1Srz5YTWaR0hrvSMUqhxccrV00UgCwTFjlCJpIHjIjib2OMNs22B4OphU+Kik24nqxtwojS13McjlJLJipgUylDC7Sl52pg6JcGiSE58fd6rDpRRtz2BN4dsRMMtXX1otSAnwbMFoZ62ZDYGxIgjyhLFaPGKc5KE7g/nWeqPOzt0mXBodbCnixqs70Ss1vfwWteq3FtItCZJj8XAu34X2xDO5MWKSP1w9Vq71zmVzQDc8ORELFg0laXFL54hxaY9lp8JvkTCGi/6gV32jKGKekk99Oik9ubqb7f8qp+TMI90jQ7+MqAwlcClHes4NQ0OU3Ca+eS6yrLj4VX0TKtWgvAyiKXUs5DXKd4GqqO9HQNZyJsv5hS9Aju+1dQXh3gHLFZLeBKdiIjpPknDIPb4DPelmVusnzdrx+3YMrDjH5nAIGbPnazufbZ48UFcyQ4zwcpD6JJTD7ENOOjzVVPptNzEEh85NBS5zPrgCNVkz48RRWaPArKCP67Jql+J5ucvI/GWa4MPuTb9LeIl5//0gnMjl18dZ/rh4ZxCY3ehW/9iPk+xYHz2g95HH31ZhAcmSP3WjwjId3gbXX+9X6si6zc3EovsRdPFV5qkj7ychnjiRcd+aWVPC1TKGnDtIdaqQfAJPWi0ZIdbmzMEXKasTYM73Fvm4Anr0bNoLveOpXRD77rs0dF046vYkhRkpm88NNiUz2zYFzI8pWgPXTJjhK0=

At 2017-12-15T17:27:42+01:00, Emilio Jesús Gallego Arias wrote:

> $ make plugins/ltac/ltac_plugin.cmxs

I did "make coqbinaries plugins/ltac/ltac_plugin.cmxs tools", but when
I tried to compile my files after that, I got an error "cannot guess a
path for Coq libraries; please use -coqlib option". I think I will
stick with "make coqbinaries states tools".

Best regards,
Raghu.

--
N. Raghavendra
<raghu AT hri.res.in>,
http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/

[Coq-Club] Makefile targets, N. Raghavendra, 12/15/2017
- Re: [Coq-Club] Makefile targets, Gaëtan Gilbert, 12/15/2017
  - Re: [Coq-Club] Makefile targets, N. Raghavendra, 12/15/2017
- Re: [Coq-Club] Makefile targets, Emilio Jesús Gallego Arias, 12/15/2017
  - Re: [Coq-Club] Makefile targets, N. Raghavendra, 12/15/2017
    - Re: [Coq-Club] Makefile targets, Gaëtan Gilbert, 12/15/2017
      - Re: [Coq-Club] Makefile targets, N. Raghavendra, 12/15/2017
    - Re: [Coq-Club] Makefile targets, Emilio Jesús Gallego Arias, 12/15/2017