lp:~ezyang/coq/trunk

Branch merges

This import branch has no branches proposed for merge into it.

No branches dependent on this one.

Related source package recipes

2 recipes using this branch. (?)

Related snap packages

Related bugs

Related blueprints

17528. By Pierre-Marie Pédrot <email address hidden> on 2016-06-15

Fix test-suite for opened bug #4813.

17527. By Matej Kosik <email address hidden> on 2016-06-15

typography

17526. By Pierre Letouzey on 2016-06-15

ocamllibdep + coqdep : simpler deps concerning .mllib and .mlpack

 Since we already have a rule %.cmxs:%.cmxa and the .cmxa depends
 already on all the .cmx inside it, no need to state explicitely
 that the .cmxs depends on these inner .cmx. Same thing concerning
 .cmxs built out of a single .cmx.

17525. By Pierre Letouzey on 2016-06-15

Makefile.build: ensure a build failure in case of a missing rule

 Earlier (as in #4812), a target with some declared dependencies (e.g.
 in a .d) but no building rule would lead to a successful build,
 even though it is actually incomplete.

 Side effect: it is now mandatory to declare phony targets in a
 .PHONY statement.

17524. By Enrico Tassi on 2016-06-15

fix test-suite/ide Makefile (stupid typo)

17523. By Emilio Jesus Gallego Arias <email address hidden> on 2016-06-14

Preventive compatibility fixes for flushing.

In pre 8.6, `Pp` provided its own reimplementation of
`Pervasives.flush_all`, with different semantics.

Unfortunately, with the removal of `Pp.flush_all` in #179, a couple of
points were silently switched to the `Pervasives` version, which may
lead to some subtle printing differences.

As a preventive measure, we restore the same semantics for these parts
of the codebase.

Note that we don't re-introduce Coq's `flush_all` for several reasons:

- Consumers of the logging API should not mess with flushing and
  Formatters as this is backend dependent (i.e: when in IDEs).

  Use of `Format` should be fully encapsulated if we want some hope of
  IDEs taking full control.

- As used, the old semantics of `flush_all` were fragile.

17522. By Emilio Jesus Gallego Arias <email address hidden> on 2016-06-14

Fix for bug #4784

We revert the change of flushing strategy in the toplevel.

PR #179 introduced a different flushing in toplevel, but it creates
problems as new lines appear when Set Printing Width is large and proof
general complains, see bugzilla#4784. The use of `flush_all` also
produces missing output.

IMO, this is a pitfall of the current setup, in particular, `Format` is
used without enclosing expressions in top-level boxes, as required. This
results in undefined behavior and fragile printing such as this bug
exemplifies.

Test suite passes.

17521. By Pierre Letouzey on 2016-06-14

Repair the build of ide/coqidetop.cmxs (fix #4812)

 Restore the .cmxa-->.cmxs rule from the Makefile. Sorry, I was thinking
 that all plugins would now be built from .mlpack (hence using only the
 .cmx-->.cmxs rule), and I forgot about this coqidetop business.

 Now the really intersting question is : why on earth 'make world' was
 silently failing to build this file but succeeding nonetheless ?!

17520. By Enrico Tassi on 2016-06-14

Merge remote-tracking branch 'origin/pr/166' into trunk

Add -o option to coqc

17519. By Enrico Tassi on 2016-06-14

Merge remote-tracking branch 'origin/pr/205' into trunk