coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Configuring CoqIDE for multiple file projects

From: Kenneth Roe <kendroe AT hotmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Configuring CoqIDE for multiple file projects
Date: Tue, 30 May 2017 17:28:24 +0000
Accept-language: en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=kendroe AT hotmail.com; spf=Pass smtp.mailfrom=kendroe AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM03-CO1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:ft+NyR+y3OYNff9uRHKM819IXTAuvvDOBiVQ1KB42uscTK2v8tzYMVDF4r011RmSDNudtq0My7KP9fuxBipYudfJmUtBWaIPfidGs/lepxYnDs+BBB+zB9/RRAt+Iv5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkJ6KevvB4Hdkdm82fys9J3PeQVIgye2ba9vIBmsowjcssgbjZFiJ6sz1xDFpmdEd/lMyW5mIV+enQzw6tus8JJm7i9dp+8v+8lcXKr1eKg1UaZWADM6PW4r+cblrwPDTQyB5nsdVmUZjB9FCBXb4R/5Q5n8rDL0uvJy1yeGM8L2S6s0WSm54KdwVBDokiYHOCUn/2zRl8d9kbhUoBOlpxx43o7UfISYP+dwc6/BYd8XQ3dKU8BMXCJDH4y8dZMCAeofM+hFs4nzqVgAogexCgS3Huzj1iNEi2Xq0aEmzugsFxzN0gw6H9IJtXTZtND7O7kUUeCz0qbI0TXDZO5K1zf69ofDbxcsofKSUrJ2bMXR004vGB3eg1WQrozlIzaV2f4Ms2if9eZvSeWvi2s+pgx3vzOhxd8sh5HGi44J0FzJ8Tt1zJw3KNGiTEN2btipG4ZKuS6ALYt5WMYiTnlouCkkzr0Gvoa2cjAWxZog2xLSZeWLfpaR7B7+TeqRJix3i2x/dLK4mhay7VOvyurhVsmyzVlGtDJFksPLtnARyRPc9tSHSvp6/kenwzqP0B3T6v1AIUAzkqrbKIQtzaI3lpoWqUjDHyn2l1vqjKKOeUgo5vKk5uD5brn8pJKQLYt5hw7mPqQrgMO/AOA4MgYUX2ic/OSxzL7j8lP/QLpXlP02lbfWvYvaJcQcuq65BhVa0ocn6xqlEzim19EYkWEdLF1ZYBKHk5TpO1bWLf/kCve/mk2gnytvx/DbJbLsGY7NL3jGkLf5Z7lx8U9cyAwpzdBe/Z1YEL8BIOigEnP24ZbTCQZ8OAipyc7mDs9838UQQyjHVqSeKebZtUKCzuMpOeiFIoEP7mXTMf8gst3ji3k0hV9VR66klc8UZXa0BPNrC0WefX/lg9NHGmAP6FltBNf2gUGPBGYAL025WLgxs2k2
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

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