coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] -o option has stopped working for directories

From: Théo Zimmermann <theo.zimmi AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] -o option has stopped working for directories
Date: Mon, 07 May 2018 14:43:39 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua0-f172.google.com
Ironport-phdr: 9a23:/73rShW3yphe/hof9p9c7TXgqKLV8LGtZVwlr6E/grcLSJyIuqrYYxCBt8tkgFKBZ4jH8fUM07OQ7/i7HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba98IRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W7YhMx/jqJVrhyiqRJi3YDbfJqYO+Bicq7HZ94WWXZNU8RXWidcAo28dYwPD+8ZMOhGr4n6vVwOogO9CgmtAePvzyFHhmXz3aIg1eQhFxzN0Qs8H9IOrnvUq8/5NaYTUeCwyanIzC7Ob/xT2Tjn6YjIdgotru2LXbJ1aMfcz1QkGQ3CjlWVs4PlPjWV2/wCs2ia8+pgVf+vhHU9pw5tpTivw8EhgZTKiIIN0l3I6zl1zYIvKdC7SEN3e8CoHIZSui2AKod7QN0uTmd1sygg0LIGo4S0fC0SxZQn2RHfb/uHfpCN4h35VeaRJS50hG9/d76jnhqy/1Wsx+/iWsWu31ZKqS1FktbItn8TzRDc9s+HSv5l8keg3zaAyRzT5/laLUwokafXMZ0sz74qmpYNrEjOHDX6lFj0gaOIbkkk//Kn6+XjYrXovJ+cMIp0hxniMqQuhMO/Bv40MwkPX2ie/OS81abu/UL8QLpQj/02lrPVv4zdJcQevqK5GRNa0p4/6xajCDeryMgXnX4eLF5cZB2Hi5XpNErVLfDjDfa/hkysny1xy/DHOL3hGJTNIWLZnLfvZ7Yuo3JbnQE01JVU449eIrAHOvP6HEHr5/LCCRpsDww1xNHVCdB425kbUGSJSvuFMK7V902J4+cuC+aJbY4R/j36Lq52tLbVkXYllApFLuGS1pwNZSXgR6U0EwCieXPpx+w5PyIPtws6QvbtjQTbAzFWbne2Gak742NiUd70PcL4XomoxYe58mKjBJQPPzJJD1mNFTHjcIDWA65ROhLXGddol3k/bZbkS4Il0kvw5grzyr4iM+OMvyNB6sil299y6One0xo18G4sAg==

Dear Chris,

This is clearly a regression. We advise that you open a bug report at https://github.com/coq/coq/issues so that this can receive a proper answer (i.e. a bug fix, hopefully ready for 8.8.1).

Thanks,

Théo

Le lun. 7 mai 2018 à 16:13, Chris Dams <chris.dams.nl AT gmail.com> a écrit :

Dear all,

Since I updated to coq 8.8.0, the -o option is no longer working like it used to. I am using this option to have a separate build directory, so my Makefile produces a command like
coqc -R . Lib -o build/directory/file.vo directory/file.v. This used to work but this is no longer the case. Instead it creates file.vo in the same directory as file.v.

Kind Regards,
Chris

[Coq-Club] -o option has stopped working for directories, Chris Dams, 05/07/2018
- Re: [Coq-Club] -o option has stopped working for directories, Théo Zimmermann, 05/07/2018
  - Re: [Coq-Club] -o option has stopped working for directories, Chris Dams, 05/07/2018