<feed xmlns='http://www.w3.org/2005/Atom'>
<title>coq/config/Makefile.template, branch master</title>
<subtitle>The formal proof system</subtitle>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/'/>
<entry>
<title>configure: add support of MinGW Win32 environment (fix #2526)</title>
<updated>2012-05-23T13:37:51+00:00</updated>
<author>
<name>letouzey</name>
</author>
<published>2012-05-23T13:37:51+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=d05961c7e6cb4a2f8cb70b136f58ef3dee2a9b32'/>
<id>d05961c7e6cb4a2f8cb70b136f58ef3dee2a9b32</id>
<content type='text'>
 * Since MinGW/Msys doesn't provide a cygpath utility, we emulate
   it via an ocaml script tools/mingwpath.ml
 * Avoid the crazy sed portions for backslash escaping, instead use
   a more robust ocaml script tools/escape_string.ml based on
   String.escaped
 * No more config/Makefile.template + sed on it, but rather a
   "cat &lt;&lt; EOF &gt; ..." as for config/coq_config.ml
 * Normally, support of Cygwin should be preserved, as well as
   mingw32 cross-compilation from linux (cf. myocamlbuild.ml)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15348 85f007b7-540e-0410-9357-904b9bb8a0f7
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
 * Since MinGW/Msys doesn't provide a cygpath utility, we emulate
   it via an ocaml script tools/mingwpath.ml
 * Avoid the crazy sed portions for backslash escaping, instead use
   a more robust ocaml script tools/escape_string.ml based on
   String.escaped
 * No more config/Makefile.template + sed on it, but rather a
   "cat &lt;&lt; EOF &gt; ..." as for config/coq_config.ml
 * Normally, support of Cygwin should be preserved, as well as
   mingw32 cross-compilation from linux (cf. myocamlbuild.ml)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15348 85f007b7-540e-0410-9357-904b9bb8a0f7
</pre>
</div>
</content>
</entry>
<entry>
<title>Tentative and very experminental support for typerex. Enabled with</title>
<updated>2012-05-11T15:11:07+00:00</updated>
<author>
<name>aspiwack</name>
</author>
<published>2012-05-11T15:11:07+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=5ea279dbd47d9ef1b87351e4df469aba3310f3f0'/>
<id>5ea279dbd47d9ef1b87351e4df469aba3310f3f0</id>
<content type='text'>
./configure -typerex .

It causes (non-fatal) errors when compiling files without a .mli (the problem
seems to have something to do with the flag -intf-suffix .cmi).

In practice, most typerex functionalities don't work well because typerex
fails its lookup into files compiled with -rectypes.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15302 85f007b7-540e-0410-9357-904b9bb8a0f7
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
./configure -typerex .

It causes (non-fatal) errors when compiling files without a .mli (the problem
seems to have something to do with the flag -intf-suffix .cmi).

In practice, most typerex functionalities don't work well because typerex
fails its lookup into files compiled with -rectypes.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15302 85f007b7-540e-0410-9357-904b9bb8a0f7
</pre>
</div>
</content>
</entry>
<entry>
<title>./configure &amp; freedesktop</title>
<updated>2011-12-18T22:50:06+00:00</updated>
<author>
<name>pboutill</name>
</author>
<published>2011-12-18T22:50:06+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=a428f79ca9ddacb4650c4a6bda7aa231e11d92ae'/>
<id>a428f79ca9ddacb4650c4a6bda7aa231e11d92ae</id>
<content type='text'>
1/ man dir is now prefix/share/man and not prefix/man git diff!
2/ a data dir option for coqide extra data.
3/ typo

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14821 85f007b7-540e-0410-9357-904b9bb8a0f7
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
1/ man dir is now prefix/share/man and not prefix/man git diff!
2/ a data dir option for coqide extra data.
3/ typo

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14821 85f007b7-540e-0410-9357-904b9bb8a0f7
</pre>
</div>
</content>
</entry>
<entry>
<title>coqide default pref files are by default in /etc/xdg/coq/</title>
<updated>2011-11-21T16:58:35+00:00</updated>
<author>
<name>pboutill</name>
</author>
<published>2011-11-21T16:58:35+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=5e62a6a476c925e58e169e43468ed0cee422bb1a'/>
<id>5e62a6a476c925e58e169e43468ed0cee422bb1a</id>
<content type='text'>
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14715 85f007b7-540e-0410-9357-904b9bb8a0f7
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14715 85f007b7-540e-0410-9357-904b9bb8a0f7
</pre>
</div>
</content>
</entry>
<entry>
<title>Coqide Menubar integration in MacOS</title>
<updated>2011-06-10T18:35:06+00:00</updated>
<author>
<name>pboutill</name>
</author>
<published>2011-06-10T18:35:06+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=6858036c6d12d77df2da9643b04f56733428be13'/>
<id>6858036c6d12d77df2da9643b04f56733428be13</id>
<content type='text'>
Because of lablgtk issues, accel_maps can't be customized well on MacOS

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14180 85f007b7-540e-0410-9357-904b9bb8a0f7
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
Because of lablgtk issues, accel_maps can't be customized well on MacOS

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14180 85f007b7-540e-0410-9357-904b9bb8a0f7
</pre>
</div>
</content>
</entry>
<entry>
<title>Coqide: a special kill function for win32</title>
<updated>2011-04-21T16:12:57+00:00</updated>
<author>
<name>letouzey</name>
</author>
<published>2011-04-21T16:12:57+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=e1d0e7cd11cfe63f4741274f6d94f07887f32ffe'/>
<id>e1d0e7cd11cfe63f4741274f6d94f07887f32ffe</id>
<content type='text'>
 This is implemented as a C external launching the TerminateProcess
 of the Win32 API. This should be considered as quite experimental
 (cf. the way we handle pid in the comment of ide_win32_stubs.c).

 I don't know how to emulate an interrupt (Ctrl-C), for now the two
 button "Restart" and "Interrupt" have the same semantics on win32
 (kill the subprocess and start at top).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14044 85f007b7-540e-0410-9357-904b9bb8a0f7
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
 This is implemented as a C external launching the TerminateProcess
 of the Win32 API. This should be considered as quite experimental
 (cf. the way we handle pid in the comment of ide_win32_stubs.c).

 I don't know how to emulate an interrupt (Ctrl-C), for now the two
 button "Restart" and "Interrupt" have the same semantics on win32
 (kill the subprocess and start at top).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14044 85f007b7-540e-0410-9357-904b9bb8a0f7
</pre>
</div>
</content>
</entry>
<entry>
<title>MacOS integration</title>
<updated>2011-01-07T14:26:38+00:00</updated>
<author>
<name>pboutill</name>
</author>
<published>2011-01-07T14:26:38+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=2b636a03f937fcb6739f48f10b60323d80a84bca'/>
<id>2b636a03f937fcb6739f48f10b60323d80a84bca</id>
<content type='text'>
if `pkg-config --exists ige-mac-integration`, coqide.opt will be
able to open files by double-clik in finder on Darwin.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13779 85f007b7-540e-0410-9357-904b9bb8a0f7
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
if `pkg-config --exists ige-mac-integration`, coqide.opt will be
able to open files by double-clik in finder on Darwin.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13779 85f007b7-540e-0410-9357-904b9bb8a0f7
</pre>
</div>
</content>
</entry>
<entry>
<title>TeX input method is now supported upstream</title>
<updated>2010-10-07T15:07:27+00:00</updated>
<author>
<name>vgross</name>
</author>
<published>2010-10-07T15:07:27+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=334cbcdffd811135cbc282ef1eace1bc69b0ccbd'/>
<id>334cbcdffd811135cbc282ef1eace1bc69b0ccbd</id>
<content type='text'>
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13514 85f007b7-540e-0410-9357-904b9bb8a0f7
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13514 85f007b7-540e-0410-9357-904b9bb8a0f7
</pre>
</div>
</content>
</entry>
<entry>
<title>Add (almost) compatibility with camlp4, without breaking support for camlp5</title>
<updated>2010-05-19T15:29:48+00:00</updated>
<author>
<name>letouzey</name>
</author>
<published>2010-05-19T15:29:48+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=1b089eb0231b4bd6d4cafb30f9e051bb53665978'/>
<id>1b089eb0231b4bd6d4cafb30f9e051bb53665978</id>
<content type='text'>
The choice between camlp4/5 is done during configure with flags
 -usecamlp5 (default for the moment) vs. -usecamlp4.

 Currently, to have a full camlp4 compatibility, you need to change
 all "EXTEND" and "GEXTEND Gram" into "EXTEND Gram", and change "EOI"
 into "`EOI" in grammar entries. I've a sed script that does that
 (actually the converse), but I prefer to re-think it and check a few
 things before branching this sed into the build mechanism.

 lib/compat.ml4 is heavily used to hide incompatibilities between camlp4/5
 and try to propose a common interface (cf LexerSig / GrammarSig).
 A few incompatible quotations have been turned into underlying code
 manually, in order to make the IFDEF CAMLP5 THEN ... ELSE ... END
 parsable by both camlp4 and 5. See in particular the fate of
 &lt;:str_item&lt; declare ... end &gt;&gt;

 Stdpp isn't used anymore, but rather Ploc (hidden behind local module Loc).
 This forces to use camlp5 &gt; 5.01.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13019 85f007b7-540e-0410-9357-904b9bb8a0f7
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
The choice between camlp4/5 is done during configure with flags
 -usecamlp5 (default for the moment) vs. -usecamlp4.

 Currently, to have a full camlp4 compatibility, you need to change
 all "EXTEND" and "GEXTEND Gram" into "EXTEND Gram", and change "EOI"
 into "`EOI" in grammar entries. I've a sed script that does that
 (actually the converse), but I prefer to re-think it and check a few
 things before branching this sed into the build mechanism.

 lib/compat.ml4 is heavily used to hide incompatibilities between camlp4/5
 and try to propose a common interface (cf LexerSig / GrammarSig).
 A few incompatible quotations have been turned into underlying code
 manually, in order to make the IFDEF CAMLP5 THEN ... ELSE ... END
 parsable by both camlp4 and 5. See in particular the fate of
 &lt;:str_item&lt; declare ... end &gt;&gt;

 Stdpp isn't used anymore, but rather Ploc (hidden behind local module Loc).
 This forces to use camlp5 &gt; 5.01.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13019 85f007b7-540e-0410-9357-904b9bb8a0f7
</pre>
</div>
</content>
</entry>
<entry>
<title>"make source-doc" builds documentation of mli in html and pdf at</title>
<updated>2010-04-29T16:33:36+00:00</updated>
<author>
<name>pboutill</name>
</author>
<published>2010-04-29T16:33:36+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=8e66761c81648add03ed21b157a3bace716b8e08'/>
<id>8e66761c81648add03ed21b157a3bace716b8e08</id>
<content type='text'>
dev/ocamldoc/

old "make source-doc" that documents ml files and didn't work is now
"make ml-doc" but still don't work :-)

"make clean" cleans dev/ocamldoc/ properly

wierd? calls of dependency graph generation leave unchanged

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12978 85f007b7-540e-0410-9357-904b9bb8a0f7
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
dev/ocamldoc/

old "make source-doc" that documents ml files and didn't work is now
"make ml-doc" but still don't work :-)

"make clean" cleans dev/ocamldoc/ properly

wierd? calls of dependency graph generation leave unchanged

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12978 85f007b7-540e-0410-9357-904b9bb8a0f7
</pre>
</div>
</content>
</entry>
</feed>
