coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Configuring CoqIDE for multiple file projects

From: Kenneth Roe <kendroe AT hotmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Configuring CoqIDE for multiple file projects
Date: Tue, 30 May 2017 14:25:16 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=kendroe AT hotmail.com; spf=SoftFail smtp.mailfrom=kendroe AT hotmail.com; spf=None smtp.helo=postmaster AT nm1-vm6.bullet.mail.ne1.yahoo.com
Ironport-phdr: 9a23:S+Qd3BUEGiIZawLepe+CFSKeRu3V8LGtZVwlr6E/grcLSJyIuqrYbBeBt8tkgFKBZ4jH8fUM07OQ6PG+HzFfqdbZ6TZZIcMKD0dEwewt3CUeQ+e9SnfHZMbwaCI7GMkQHHRExFqcdXZvJcDlelfJqWez5zNBUj/2NA5yO/inUtWK15f/2O+94YDcbBtVjzShf7xyMA+2rQLMvcUKnIduMKg8xx/Ir3dSe+lbx35jKVaPkxrh/Mu98ppu/iZKt/4968JMVLjxcrglQ7BfEDkpPGc56dHxuxXEUQWB+GYXXH8MkhpPDQjF7RX6UYn0vyDnqOdz2zSUMNPvQ7wsVjus86lkSBnziCcaLDE5633YitZxjK1Avh2soQF0zpPOb4GUMPp+eb7dfc8fSGFcUMtdSzBND4WhZIQID+oBOvpYr4znqFsPqRuyHBCgCuPhxzJKhXL6xLA23/o8Gg3C0wEsA9cCvXLJp9v3KagSS/i4wqnUwjrMcv1Y1zn95pbKfR4ipv+BRqh/fdbUyUQ1FwPJkledpIr4ND2VzOQNtG2b4vJlW+2xjW4nrR9+oiSvxswxlofJgZwawU3D+CV63ok1I8C3SFR8YdG6C5ZQtyaaN5dzQsw4QmFovDw2xaEBuZ6+ZSUHzoksyR3Ha/Gfd4WF4QjvWPufLDp7nn5ofK+ziwys/UWgxODwTs253VVQoiZYnNTBtWoB2wLN5sWGUPdx40ms1SqJ2gvO8O9LO1o0mrDeK5M5wr4/iJ4TsUPbEy/wnUX6kbaadlsh+uWp8ejoeajmppuYN4BqlgHyKKEulda+AeQ8KAQOWXaU9fmm2Lzj50L5QLJKjvosnqbFt5DaINwXpq+/AwBLzoYu8xKyAjS83NgFk3QKL0hJdRaag4TzJV3DIP71Ae+6g1u2kTdrw/7GPqfmApXINnXDk6nufbBg5E5Gzwo808tS55JTCrEdJfL8QE7xtNjCAhAlNAy0xv7rCM9h2YMGRWKPHqiZPbvOvl+P/+IjOvWDZIsIuDnmMPUl/P7vjXohmVAHZ6Wp3J0XaGq5Hvt8OUmZb2Ds0Z89FjIBuRN7R+j3gnWDVyRSbjC8RfES/DY+XaGrC4HOWoDluruMlHO4E5tafGdLIlCLDXLhdoHCUPAJPnHBavR9myAJAODyA7Qq0guj4VOixg==

A bit more information. When I compile the first file, “SfLib.v”, everything works since it has no dependencies. I have another file called “SfLibExtras.v” which I open in Coq IDE. This file has “Require Export SfLib” in it. When I run the file interactively, everything seems to work. However, when I compile it, I get the error "File "/Users/kendroe/FDS/PEDANTIC/SfLibExtras.v", line 13, characters 15-20:

Error: Unable to locate library SfLib.” This only happens when I try to compile.

- Ken

On May 30, 2017, at 1:28 PM, Kenneth Roe <kendroe AT hotmail.com> wrote:

I have a Coq project with multiple files. Each file has statements such as "Require Export SfLib." to include dependencies. All source files are in the same directory. From CoqIDE, I would like to compile each of the files and be able to open one of the source files in the IDE itself. What do I need to do to configure file paths? I do not want to change the "Require" statements. I am running CoqIDE on a Mac.

- Ken

[Coq-Club] Configuring CoqIDE for multiple file projects, Kenneth Roe, 05/30/2017
- Re: [Coq-Club] Configuring CoqIDE for multiple file projects, Kenneth Roe, 05/30/2017
  - Re: [Coq-Club] Configuring CoqIDE for multiple file projects, Pierre Courtieu, 05/31/2017