coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Locate Library syntax

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Locate Library syntax
Date: Tue, 28 Apr 2020 16:39:47 +1000
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=9xv8Trul5qdI4bgMqi7Kjo6ii7gxsKSPDcOKAM42qv0=; b=ICSy5unihy7HdtrEYLO2ZTXNSan5Xrb/RzikkA0NaiPh4VpR+Cl9ggAhjV0NbzpSd3BuW+J+OD0IdI/unNFd3Y94GJxzhzvN+l1Tn/IcEcVg6/AiTyK0waUUPoVvXq0wIVLVnwKlF2bSxWmPC6IJaXt74q9vtGKuEZ5HOOfpG1hBkwneQ+uXycqGC5xgKPhDod7enZq15uRPOyNMS970zTG1tlviJGkahY5dxn5SoCvAcHAyhqC/9F/iFy9UzYSEUUuEboXMEtXdgk90GuESpYZx08bGgmTSW34MLvoW6IvUinQ8AaDqHxnL7lk2Hon21LP0YKCCP3OU4YO0CXtLUg==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=gmyACK4h5GGFTny4PviDUsoHd0t5a16nfKWc0ODJZ3WQJH+zwfDE1DqwmpCMZeZI0YWgy1Xh89mE8uzN7M8ulLkjjUdYkQl5FRuEwIPpc9OhHwUpXfqXvDQHb0IbHmTi0BoasUs6nl5y7R/9W29wHuvBGtlbS4q/OQWzpP0TRQDQ5/e/O5mt8iBg4UpxMm4gKjtnIgbnOZ1GsGyTLeJimpKbmbl8yy228Ge8KOp/fHqcXMCfng5BaCFdFxhmwgb/aaDZsI5I2KODU5Oxda8Tf3TREyNQNvHJlJVF58IL300DBe7bfh16RsF4+JmuPOn5iRhxNYo5vfavHytt8m6mDQ==
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-ME1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:nHG37hX1uaQGEvQ7PvxP2cpxDCbV8LGtZVwlr6E/grcLSJyIuqrYbBaPt8tkgFKBZ4jH8fUM07OQ7/m9HzJYqs/Z7TgrS99lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal9IRmrrQjdrMgbjZdtJqos1hfEomZDdvhLy29vOV+dhQv36N2q/J5k/SRQuvYh+NBFXK7nYak2TqFWASo/PWwt68LlqRfMTQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4qx2RhLklDsLOjgk+2zRl8d+jr9UoAi5qhJhw4DafYKbOvRwcazBct0VSmtBU91NVyFDGI6wc5cDAuQDMOtesoLzp0EOrRy7BQS0AO3g1CVIiWHz3aw6zu8vHxvJ3QI7H9IJtnTfsdL4OqMMXuCv0qbIyDXCY+lY1zjn5onIaRchofeXUL1qd8rR1FMjGB3YgVWNs4DqJS6V2/0LvmOG7ORgTfqihmE7pw1rvzSj2sUhhpPUio8by13I7zh1zYgoKdGgR0N2ZcSoHIZTui2GLYd7QM0vT3t1tCok1rELv4OwcjIQx5Q93RHfbuSKc4iW7RLnU+acOSt1i3x4dr6jmhq+6E+uxOLhWsWt11ZFtTRKnsPLtnAQyxzc8c+HSuZ7/ki8wzqPzxrT6uZYIU8qiaXbN58hwrk2lpYJtkTDAzP2mEHxjK+RdUUo4PSn6+PiYrn+p5+cMZF7ih3mP6khhsCzG/k0PhQMUmSB5Oix2rzu8VfkTLhEk/E6iqzZv4rbJcQfqK65GQhV0oM75hi7ETimysoXnXwHLV5fdhyIlYboO0rJIPD+FvqwmVKskCpxy//YI7LhH4/BIWLekLv5Z7Zy91ZcyBYvzdBY/59bFrYBIOvqVkDtsNzYEwQ2Phevw+fnDdV9zpkRVXiOAq+fKqPSsEWH6vghI+mWN8cpv2O3IP88ovXqkHURmFkHfKDv04FdICSzGe0jKEGEa1LthM0AGCEEpFxtYvbtjQigXCReYmf6c6sj/TY9QNaEAJ3OQ5HrrLWexyC9NpRQeyZLBk3KGGq+JNbMYOsFdC/HepwpqTcDT7X0E9Z9hyHrjxfzzv9cFsSR4jcR7Mix3d5ooeDfiFc76G4sVpXP4yS2V2hx21gwaXoz1aF7r1Z6zw7Zg6F+nrpVGcEV7u4bC15nZ66Z9PRzDpXJYiyEftqNTwr5EPybOmloC/ccmpoJaUs7HMi+hBfe2SbsG6USi7GAGJ0z9OTbwmT1IMF+jX3B0ft4gg==

Hi,

Trying to use the Locate Library command I get

> Locate Library existsT.
> ^^^^^^^
Error:
Syntax error: [constr:global] expected after 'Library' (in [locatable]).

I've seen this sort of gibberish before, but it's generally due to a recognizable syntax error. But here I can't seen what is wrong with the way I'm using the Locate Library command, eg

Coq < Locate Library gen.
gen is bound to file /home/jeremy/coq/lnt/tense-logic-in-Coq/gen.vo

Coq < Locate Library xxx.
Toplevel input, characters 15-18:
> Locate Library xxx.
> ^^^
Error: Unable to locate library xxx.

these work as expected - what is happening here?

Cheers,

Jeremy

[Coq-Club] Locate Library syntax, Jeremy Dawson, 04/28/2020
- Re: [Coq-Club] Locate Library syntax, Théo Zimmermann, 04/28/2020
  - Re: [Coq-Club] Locate Library syntax, Jeremy Dawson, 04/28/2020