Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Add LoadPath in Coq 8.12.2

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Add LoadPath in Coq 8.12.2


Chronological Thread 
    < Chronological >      < Thread >
  • From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Add LoadPath in Coq 8.12.2
  • Date: Wed, 20 Jan 2021 12:55:04 +1100
  • 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=JLY5h+NfDbKEXMY0t9Srhvb3pogoAi/BQogUDdfcTW8=; b=TXwlpy/xfv2mUzYoJ7u2I4UUlJp2DU1wlZP6zEN2SL9eVJWk9WyYbQcdP5D4EMMxx2arJCcrrDR3ICsWCD3P5vVeBAqsQZttI4XRSYOPM9sApasbojobMlItnnhaHeKAwrf6NFLkYLGFdlkK7qxZVwZHSymazfKbZ6Q8zmc33ws37IOE3TUBkma7W9tBFvAURThTLhh4CVQuZ01mewJguAJDuQDBOKQ5sV66neEolicMhizRXbw1kuaaWPO05QftGLp1GwIP1lbGzV5ZXSYAAb7RbJXDk2bmQhd8nqQwM1Gt0O0iSPmbQ5s29AgIsuywBnwDNJLL/nQXIxoVmVmorw==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=eoLLDSoEsPfQ/el+iT4Eyi32FEq4caA3501FDzYiQa/vIeF/AUg7IwTbkZaA9j5EzK/phwSbxW3mN39xIHRhKynFN7d3We6q+8GSqcUpbNFlazY1e7UGxlvdDnPDnwuWGgEe3IXP9oYnt9o+V3QigmH54iRQMUsZr3Xmg55pL6aS4n7muOTpYLXZPU2a0zDkPTCAh/UfbitvmD/p8D2JPIHG9DV7GA009wvn/uYIuCp5G7FvMKTXBfc4hCH/ZTJWiym/YFQVqx3fUvMPh4Yf4VtYH2d6wYwIW7JNhdGLXBjs7HgtTRXNXfLm5syQsv9aiha/iwOr6DwjhJTXtgwW+g==
  • 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-ME3-obe.outbound.protection.outlook.com
  • Ironport-phdr: 9a23:/tZPaxawXoXhNB/+M0PXiZr/LSx+4OfEezUN459isYplN5qZrsqzbnLW6fgltlLVR4KTs6sC17OH9fm5EjBYqdbZ6TZeKcMKD0dEwewt3CUYSPafDkP6KPO4JwcbJ+9lEGFfwnegLEJOE9z/bVCB6le77DoVBwmtfVEtfre9FYHdldm42P6v8JPPfQpImCC9YbRvJxmqsAndrMYbjZZmJ6or1xfFv3REdutKyWh1IV6fgwvw6t2/8ZJ+8Slcoe4t+9JFXa7nY6k2ULtUASg8PWso/sPrrx7DTQWO5nsYTGoblwdDDhbG4h/nQJr/qzP2ueVh1iaUO832Vq00Vi+576h3Uh/oiTwIOCA//WrKl8F/lqNboBampxxi347ZZZyeOfRicq/Be94RWGxMVdtTWSNcGIOxd5YBAfQPPehYrIfzqVUBohmiCgejBePgxSRFhmP00KAgz+gtDQ/L0QwmEtkTsHrUttL1NKIKXO6x0qbI1yvMb/ZW2Dzg5obHaB4goeqLXbJ2bMHczk0hGB3fjlqOrIzkPymZ2OoXvGmV9OpgUuSvhnU9pAF3vzij3NkjhZTUho4P0F/E6Dx0zYAoLtK3VEB1e8SrEIdMty6ELYt2RNsvTn1rtSskybAKpJy2cDQXxZopyRDSZfyKfoiJ7x79VuucLyp0iW94db6igxu//1asx/D8WMSq31hEoTdJn8TDuH0Lyhfd5M+HSv5n8Ueg3zaCzxrc6udZIUwui6XUNoMhzqQqmZoOt0nIAyz4mF3ugaKZakko4PWk5/jlb7n8u5OQK4x5hhvjPqgwmsGzGes1PwwUU2SG+umwyafv8VPnTLhJlPE6j6nUvZbHLsoBvKG5GRVa0oM75ha/ETim1NMYkGEbIV1LZRyLk5XlN0jJLv73A/qzmlOsnyx1yPzcOb3hH4nNIWPEkLf8e7Zy9lRQyBIpzdBY+5JbFK0OIO7yWk/2stzUFBg5MxGow+bjD9V90YAeVXiTDa+eNaPeqV6I5uQxLOmQfIIYtyrxJ+I46/Lyj3I1g0IRcbWq0JcNdXy0APRrL12cYXX2g9cBFWkKvhA5TOzvkFCMVSBcZ2ysUKI55jA3EoyoAp3NR4C2h7yB2jy2EYdQZmBbEFyDD2rnd5ieV/gWdSKeOtVhnSAcVbi9V48h0gmjuxP9y7p+N+bb5ikYtY/429Vu/O3SlRQy9SRuAMiH0mGNSXt0nmISSDMs0qB/ux819lDW2q9hxvdcCNZ75vVTUw58O4SP4fZ9DoXQVxjMe8bBZF+5WdKgSWUTQ8g8xs5IT09iANKkphnFwmynD6JTnqHdV898yb7Vw3Wkf5U18H3BzqR01wB6EPsKDnWvg+tEzyaWH5TAyh/LnqC3M6kQwWjE6TXblDfcjARjSAd1FJ79czUfa0/R8Yurz375F+brLJl8dwxLxIiFN7dAbcDvgRNeXvD/Nd/CYmW33WCtGRKPwbDKZ43vKTxEjXftTXMcmgVWxk6ocA03ByOvuWXbVWY8HFTyJU7g7K93tSHiQw==
Hi Yannick,

Here is a sample of the error message

[jeremy@localhost test]$ coqtop -color no
Welcome to Coq 8.12.2 (December 2020)

Coq < Add LoadPath "../general".
Toplevel input, characters 25-26:
> Add LoadPath "../general".
> ^
Error:
Syntax error: 'as' expected after [Prim.ne_string] (in [vernac:command]).

(The whole code isn't publically available, there's an extract of it at
http://users.cecs.anu.edu.au/~jeremy/tmp/type-error.tar
which I put there for the purpose of another query. I asserted that it should compile under 8.11 though I can't check that now. And it doesn't display the error that this thread is about, because it first hits errors resulting from other changes between 8.11 and 8.12 which I haven't addressed yet.)

Cheers,

Jeremy

On 20/1/21 2:24 am, Yannick Forster wrote:
Hi Jeremy,

what's the error message you get? Is your code publically available (on github or something similar)?

Best
Yannick

On 19 January 2021 13:52:24 Jeremy Dawson <Jeremy.Dawson AT anu.edu.au> wrote:

Hi,

I have just upgraded my operating system, which has also involved
getting Coq 8.12.2 (December 2020)

Previously I was using Coq 8.11.2

The command
Add LoadPath "../tense-lns".
now seems to cause an error.

How do I change the command to get the same behaviour?

Thanks

Jeremy


Archive powered by MHonArc 2.6.19+.

Top of Page