coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Require Import fails

From: Ian Shillito <Ian.Shillito AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Require Import fails
Date: Wed, 30 Sep 2020 02:23:45 +0000
Accept-language: en-AU, en-US
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=anu.edu.au; dmarc=pass action=none header.from=anu.edu.au; dkim=pass header.d=anu.edu.au; 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=/c6dtVkTC4Z0EKhaasNd0uqaQrOQChf7YPnrc7IWWfQ=; b=QMneUai8vnjCKVOt/nNGpOHA8sjpXuPLwRj0Z1yxBzqkGfxB7D0E3MmIVrxTBey06tn992X1CxTxfnimriG31CNvA2iaJxbbDJ9C/7e5A1kB3urYYXlSdVOcEie8U3MhFw/SM821NtnIdLvoxJJmWjvhCePwCXvKdwvsGBhP+YxEe1jXusDfOobeveZsvai+jqTODWElE8pG7Au2PaOaXSjhAE4W6TfnXtsjjRyfOa/CO0ai2wCj/++kV8vYq6fNxMe0r6mCeKbx94KG163wRULXl5EPvS5aNnQissscLSD4H83yQKWgUVeSE+64P1E7UWDKaJrsu7SiTUvd3hf+EQ==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=mYd3et5gayB8Dd1+jZEmEonggiZ5l2oLS4+bZbsOaJTy4I0tE4zieE3dVdUKWlk/3fCpPmcFK06Sxm4/QWvfqZASRwKi4BG1xADeJqGQetlbK3Uz2w8yBDAoCt7GJCCRVDCZ/pyxVC8YMLibm2VzMKZdNOlUELFn6fB0o8NGep8OyARNnKRC3BFBM96PVaYZAdYJPqER+E9W2Y1CeP5+iT4clUUi8x0QJy8+2ZbYXNoielAo72xODpN8RkoetPUCngpwD/AyN0WLXETPFr7npDykq3tEx7WPQEZ4CPv5Fi52aj+cC+PFSauZWifmWjwcQ03vmKiHKa++thKkxrh2Ww==
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Ian.Shillito AT anu.edu.au; spf=Pass smtp.mailfrom=Ian.Shillito AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-SY3-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:6QEfSBLR2AskL0vLU9mcpTZWNBhigK39O0sv0rFitYgfLfXxwZ3uMQTl6Ol3ixeRBMOHsq0C0LKd7v2ocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTiwbal8IRmqognctskbipZ+J6gszRfEvmFGcPlMy2NyIlKTkRf85sOu85Nm7i9dpfEv+dNeXKvjZ6g3QqBWAzogM2Au+c3krgLDQheV5nsdSWoZjBxFCBXY4R7gX5fxtiz6tvdh2CSfIMb7Q6w4VSik4qx2ThLjlSUJOCMj8GzPisJ+kr9VoA6vqRJ8wo7bfI6aOeFkca/BYd8XX3ZNUtpMWyFHH4iyb5EPD+0EPetArIfyvV0OpgajCwmsBePvzjtIhn7q3a09zu8sFgLI0xYmH94UrXrUrNT1NKMWUeC00KnIyi7OYOlQ2Tfg8oTHbA0uoeyWUb1qbMrc0E8iHB7KgVuMs4LqJS+V1vgTvGiB6eptTfyjhnI5pwx/oTWj28chh4bGiI8Xy13J9Dh0zYQ0KNO3VkN2Y8CoHIZfui2GOYZ7XsIvTW51tCs6xbAKpIO2cicMxZ86yRDfbPmHfJKJ4hLlTOuePzh5hHN+eLKjnBay7VKsyvb7VsSyzV1ErTJFn8HDu3wRzRDf99SLR/ln8ku81zuC1Rrf5+VALEwsiKbXN5AszqQtmpYPs0nPBDL6lUH0gaOMdUgp9fCk5/rmb7n6qJKRMpJ4hh3iPakvn8GzHPg0Pw0UUGWb/Omx0aDv8VD/Tb5XlPM5iLPZv4rfJckDpq62HQtV0oE75hujATiozcgUkWQeIFxYeh2KgZHlO1bVL//mF/u/hEmskCtwyPDBI73hBIjCImLbkLf7erZ991BTxxYvzdBe4JJUDKsNIPXuWk/tsNzYCRg5Mw+uz+n7D9V905sSWWOJAqCHLKPfqVCF6v41L+WReIMYuizxJ+Ur6vPsl3M0nVsQcbGs3ZQNaXC4GvpmI1+eYXrpmtoPEn0FvgwkQOL3iF2CUDpTZ3KzX6Ig4TE2E5ipDYHeRoy3nrOOwTq7EodMaWBbElyMC2vnd52YW/cQbyKfOtNukjsdVbS4V4Ah0QyuuxThxrp8LuvU/zUYuoj52Nh04e3TjxAy+iZuA8STyWHeB11zyykDQCZz16Riq2R8zE2C2O52mbYQQddU/rZCVhowHZ/a1e1zTd7oDFHvZNCMHXevRJ2dATA1StMtxJdaQk97Xe6ijxTH3jatK7YTivqGCIFy+7+KjCu5HNp013uTjPpptFIhWMYabTT31J46zBDaAsvyq2vckq+rcaoG2yuUrjWKy3fIsU1FFgdtA/ycASIvI3DOpNG83XvsCqe0AO19YAJH1IiPJrYMY8C71QwbFsemA8zXZieKo0n1BRuMwe/TPqPXQD1EmR7sUw0DmQ1V+muaPw8jACvnu3jZEDFlCVPoZQXr7PV6r3S4CEQzylPTYg==

Hi all,

I recently started using Coq and I am facing a problem with the Require Import command. Let me explain you the situation.

First, I am working with CoqIDE_8.12.0 on a Mac.

Second, in a folder called "Test" I create a file called existsT.v. It is a very simple file only defining notations and calling no other library/file. I compile-buffer it, creating the .vo .vos .vok .glob files.

Now I create a new blank lol.v file in the same folder and write the command "Require Import existsT." and save it.

When I try to compile lol.v Coq complains: "Unable to locate library existsT. (While searching for a .vos file.)".

I saw in various places that people fix this problem by adding a load path, so this is what I do: "Add LoadPath "Users/IanShillito/Desktop/Test" as Fmz.". Note that Coq will not let me delete "as Fmz" as it complains that the syntax of the command Add LoadPath requires a name for the path.

With this load path in hand I can then write the command: "From Fmz Require Import existsT.". Once again Coq complains: "The file /Users/IanShillito/Desktop/Test/existsT.vo contains library existsT and not library Fmz.existsT".

So now Coq knows where to look (as it found the existsT.vo file) but it is looking for an overspecified name of file.

It seems like this problem is similar to the one exhibited in a recent series of email, but as I am a beginner in Coq I do not fully understand how I can extract a solution from this discussion. Can someone help me out?

Best,

Ian Shillito

[Coq-Club] Require Import fails, Ian Shillito, 09/30/2020