Opened 10 years ago

Closed 9 years ago

#363 closed defect (fixed)

Multiple file handling for Coq needs sensible treatment

Reported by: David Aspinall Owned by: David Aspinall
Priority: major Milestone: PG-Emacs-4.1
Component: 2:pg-emacs Keywords:
Cc:

Description

We need to find a way to make Proof General development across multiple files mesh smoothly with Coq users' main Makefile-based batch build mechanism. In particular, undoing across completed scripts should behave consistently and work with Coq's top level.

Change History (3)

comment:1 Changed 10 years ago by David Aspinall

Milestone: PG-Emacs-4.0PG-Emacs-4.1
Status: newaccepted

Postponing this improvement for this release.

Have discussed this with Pierre and he considers it something that is not a priority (Coq users should understand the way things work and figure it out). But it would be nice to document the recommended ways of working, perhaps, to help new users.

There is some old email to mine discussing various possible clean solutions.

comment:2 Changed 10 years ago by David Aspinall

Work in progress by Hendrik Tews on this, see http://askra.de/software/multiple-coq/ for experimental patch.

comment:3 Changed 9 years ago by David Aspinall

Resolution: fixed
Status: acceptedclosed

Hendrik's patch is now incorporated. Works nicely!

Note: See TracTickets for help on using tickets.