<feed xmlns='http://www.w3.org/2005/Atom'>
<title>coq/coq.itarget, branch master</title>
<subtitle>The formal proof system</subtitle>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/'/>
<entry>
<title>Officially discontinue the experimental coq build via ocamlbuild</title>
<updated>2016-06-08T12:32:56+00:00</updated>
<author>
<name>Pierre Letouzey</name>
</author>
<published>2016-06-01T23:22:41+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=1d6d0060330197896748739a625d0b1c7f083da2'/>
<id>1d6d0060330197896748739a625d0b1c7f083da2</id>
<content type='text'>
 It has been accidentaly broken since early 2014 (and especially
 in 8.5), no easy repair, I won't devote any more hours to this stuff.
 Moreover no one seems to care apart from Emilio, but he's ok to work
 on this in a separate repository or branch.
 I left a dev/doc/ocamlbuild.txt file with a few words about this
 experiment.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
 It has been accidentaly broken since early 2014 (and especially
 in 8.5), no easy repair, I won't devote any more hours to this stuff.
 Moreover no one seems to care apart from Emilio, but he's ok to work
 on this in a separate repository or branch.
 I left a dev/doc/ocamlbuild.txt file with a few words about this
 experiment.
</pre>
</div>
</content>
</entry>
<entry>
<title>Ocamlbuild: try to speed-up error detection in *.ml*, by byte-compiling first</title>
<updated>2010-06-03T17:13:49+00:00</updated>
<author>
<name>letouzey</name>
</author>
<published>2010-06-03T17:13:49+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=f77f93ecef9362548dae8886affe7a4bdcc150f6'/>
<id>f77f93ecef9362548dae8886affe7a4bdcc150f6</id>
<content type='text'>
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13064 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@13064 85f007b7-540e-0410-9357-904b9bb8a0f7
</pre>
</div>
</content>
</entry>
<entry>
<title>Ocamlbuild: improvements suggested by N. Pouillard</title>
<updated>2009-04-03T14:51:52+00:00</updated>
<author>
<name>letouzey</name>
</author>
<published>2009-04-03T14:51:52+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=141a21da29216a43eb067ef0fcb9c7d914d45bdc'/>
<id>141a21da29216a43eb067ef0fcb9c7d914d45bdc</id>
<content type='text'>
 * Import of Coq_config via myocamlbuild_config.ml, instead of my get_env
 * As a consequence, we enrich this Coq_config with stuff that was
   only in config/Makefile
 * replace the big ugly find by some dependencies against source files
 * by the way: build csdpcert, with the right aliases.

I've tried to escape things properly for windows in ./configure,
but this isn't fully tested yet.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12046 85f007b7-540e-0410-9357-904b9bb8a0f7
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
 * Import of Coq_config via myocamlbuild_config.ml, instead of my get_env
 * As a consequence, we enrich this Coq_config with stuff that was
   only in config/Makefile
 * replace the big ugly find by some dependencies against source files
 * by the way: build csdpcert, with the right aliases.

I've tried to escape things properly for windows in ./configure,
but this isn't fully tested yet.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12046 85f007b7-540e-0410-9357-904b9bb8a0f7
</pre>
</div>
</content>
</entry>
<entry>
<title>ocamlbuild: many improvements (macos 10.5 fix, correct dllpath, etc)</title>
<updated>2009-03-29T15:40:27+00:00</updated>
<author>
<name>letouzey</name>
</author>
<published>2009-03-29T15:40:27+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=301d6bfcf3e804d35b1fe56d569b2a11187fa5b1'/>
<id>301d6bfcf3e804d35b1fe56d569b2a11187fa5b1</id>
<content type='text'>
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12033 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@12033 85f007b7-540e-0410-9357-904b9bb8a0f7
</pre>
</div>
</content>
</entry>
<entry>
<title>Ocamlbuild: 1st reasonably complete version (rules for binaries + plugins + vo)</title>
<updated>2009-03-26T19:31:40+00:00</updated>
<author>
<name>letouzey</name>
</author>
<published>2009-03-26T19:31:40+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=d1e8a2a6e5e2fdea6cf0ff0ed9860b98eced0c97'/>
<id>d1e8a2a6e5e2fdea6cf0ff0ed9860b98eced0c97</id>
<content type='text'>
  Dealing with .vo files was harder than anticipated (issues with
  coqdep_boot and the location of the .v files). Current solution
  cannot compete for a beauty prize, but well.

  Several other issues remain (see top and bottom of myocamlbuild.ml)
  - For the moment the coqlib / coqsrc in Coq_config is to be
    hacked by hand to add _build/ in it.
  - Parallelism is a "no go" for the moment. Ocamlbuild accepts
    a -j option, but it has almost no effect experimentally.
    (but at least it doesn't take more time than make -j1,
     i.e. about 14 min here, instead of about 7 for make -j2)
  - After a first full build, ocamlbuild is awfully slow
    to detect that nothing has to be redone (1 min 25 here)

  To be continued...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12021 85f007b7-540e-0410-9357-904b9bb8a0f7
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
  Dealing with .vo files was harder than anticipated (issues with
  coqdep_boot and the location of the .v files). Current solution
  cannot compete for a beauty prize, but well.

  Several other issues remain (see top and bottom of myocamlbuild.ml)
  - For the moment the coqlib / coqsrc in Coq_config is to be
    hacked by hand to add _build/ in it.
  - Parallelism is a "no go" for the moment. Ocamlbuild accepts
    a -j option, but it has almost no effect experimentally.
    (but at least it doesn't take more time than make -j1,
     i.e. about 14 min here, instead of about 7 for make -j2)
  - After a first full build, ocamlbuild is awfully slow
    to detect that nothing has to be redone (1 min 25 here)

  To be continued...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12021 85f007b7-540e-0410-9357-904b9bb8a0f7
</pre>
</div>
</content>
</entry>
<entry>
<title>ocamlbuild: coqide, coqchk, a bit of .vo</title>
<updated>2009-03-26T12:26:52+00:00</updated>
<author>
<name>letouzey</name>
</author>
<published>2009-03-26T12:26:52+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=058c05ce14affba12eff11550016efaefc6a4747'/>
<id>058c05ce14affba12eff11550016efaefc6a4747</id>
<content type='text'>
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12019 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@12019 85f007b7-540e-0410-9357-904b9bb8a0f7
</pre>
</div>
</content>
</entry>
<entry>
<title>ocamlbuild improvements + minor makefile fix</title>
<updated>2009-03-24T18:21:07+00:00</updated>
<author>
<name>letouzey</name>
</author>
<published>2009-03-24T18:21:07+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=6a14070e4666cc8c0457b03c81ea99a9a6c4b833'/>
<id>6a14070e4666cc8c0457b03c81ea99a9a6c4b833</id>
<content type='text'>
 * a small shell script ./build to drive ocamlbuild
 * rules for all the binaries (apart from coqide and coqchk)
 * use of ocamlbuild's Echo instead of using shell + sed + awk
   for generated files
 * Makefile: remove unused STAGE1_CMO and add bin/coqdep_boot to the
   list of things to "clean"

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12012 85f007b7-540e-0410-9357-904b9bb8a0f7
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
 * a small shell script ./build to drive ocamlbuild
 * rules for all the binaries (apart from coqide and coqchk)
 * use of ocamlbuild's Echo instead of using shell + sed + awk
   for generated files
 * Makefile: remove unused STAGE1_CMO and add bin/coqdep_boot to the
   list of things to "clean"

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12012 85f007b7-540e-0410-9357-904b9bb8a0f7
</pre>
</div>
</content>
</entry>
<entry>
<title>Many changes in the Makefile infrastructure + a beginning of ocamlbuild</title>
<updated>2009-03-20T20:50:44+00:00</updated>
<author>
<name>letouzey</name>
</author>
<published>2009-03-20T20:50:44+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=dffb6159812757ba59e02419b451e6135d1e3502'/>
<id>dffb6159812757ba59e02419b451e6135d1e3502</id>
<content type='text'>
 * generalize the use of .mllib to build all cma, not only in plugins/
 * the .mllib in plugins/ now mention Bruno's new _mod.ml files
 * lots of .cmo enumerations in Makefile.common are removed, since
   they are now in .mllib
 * the list of .cmo/.cmi can be retreive via a shell script line,
   see for instance rule install-library
 * Tolink.core_objs and Tolink.ide now contains ocaml _modules_, not
   _files_
 * a -I option to coqdep_boot allows to control piority of includes
   (some files with the same names in kernel and checker ...)

 This is quite a lot of changes, you know who to blame / report to
 if something breaks.

 ... and last but not least I've started playing with ocamlbuild.
 The myocamlbuild.ml is far from complete now, but it already allows
 to build coqtop.{opt,byte} here. See comments at the top of
 myocamlbuild.ml, and don't hesitate to contribute, either for completing
 or simplifying it !

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12002 85f007b7-540e-0410-9357-904b9bb8a0f7
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
 * generalize the use of .mllib to build all cma, not only in plugins/
 * the .mllib in plugins/ now mention Bruno's new _mod.ml files
 * lots of .cmo enumerations in Makefile.common are removed, since
   they are now in .mllib
 * the list of .cmo/.cmi can be retreive via a shell script line,
   see for instance rule install-library
 * Tolink.core_objs and Tolink.ide now contains ocaml _modules_, not
   _files_
 * a -I option to coqdep_boot allows to control piority of includes
   (some files with the same names in kernel and checker ...)

 This is quite a lot of changes, you know who to blame / report to
 if something breaks.

 ... and last but not least I've started playing with ocamlbuild.
 The myocamlbuild.ml is far from complete now, but it already allows
 to build coqtop.{opt,byte} here. See comments at the top of
 myocamlbuild.ml, and don't hesitate to contribute, either for completing
 or simplifying it !

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