<feed xmlns='http://www.w3.org/2005/Atom'>
<title>coq/dev/base_db, branch master</title>
<subtitle>The formal proof system</subtitle>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/'/>
<entry>
<title>[build] Refactoring to config lib and ocamldebug tweaks.</title>
<updated>2018-10-22T22:42:04+00:00</updated>
<author>
<name>Emilio Jesus Gallego Arias</name>
</author>
<published>2018-10-17T13:24:15+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=1db19a8f454e0f8c5a60101c87ccd38e0883d530'/>
<id>1db19a8f454e0f8c5a60101c87ccd38e0883d530</id>
<content type='text'>
We make `config` into a properly library. This is more uniform and
useful for some clients. This also matches what was done in Dune.

Next step would be to push dependencies on `Coq_config` upwards, only
the actual toplevel binaries should depend on it.

We also remove the stale `camlp5.dbg` and refactor the dbg files a
bit, isolating the bits that are specific to the plugin / lib building
method used by makefile.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
We make `config` into a properly library. This is more uniform and
useful for some clients. This also matches what was done in Dune.

Next step would be to push dependencies on `Coq_config` upwards, only
the actual toplevel binaries should depend on it.

We also remove the stale `camlp5.dbg` and refactor the dbg files a
bit, isolating the bits that are specific to the plugin / lib building
method used by makefile.
</pre>
</div>
</content>
</entry>
<entry>
<title>No more dev/printers.cma</title>
<updated>2016-07-26T14:32:49+00:00</updated>
<author>
<name>Pierre Letouzey</name>
</author>
<published>2016-07-25T13:56:24+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=32be84c5ba384f93b350a551d7bbbeec03768046'/>
<id>32be84c5ba384f93b350a551d7bbbeec03768046</id>
<content type='text'>
 This file was only used during ocamldebug sessions (in the dev/db
 script). It was containing a large subset of the core cma files,
 up to the printing functions. There were a few notable exceptions,
 for instance no kernel/vm.cmo to avoid loading dllcoqrun.so in ocamldebug.
 But printers.cma was troublesome to maintain : almost each time an ML file
 was added/removed/renamed in the core of Coq, dev/printers.mllib
 had to be edited, in addition to the directory-specific .mllib
 (kernel/kernel.mllib and co). So I propose here to kill this file,
 and put instead in dev/db several "load_printer" of the core cma files.

 For that to work, we need to compile kernel/kernel.cma with the right
 -dllib and -dllpath options, but that shouldn't hurt (on the contrary).
 We also source now the camlpX cma in dev/db, via a new generated file
 dev/camlp4.dbg containing a load_printer of either gramlib.cma or
 camp4lib.cma.

 If one doesn't want to perform the whole "source db" at the start
 of an ocamldebug session, then the former "load_printer printers.cma"
 could be replaced by:

  source core.dbg
  load_printer top_printers.cmo

 See for instance the minimal dev/base_db.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
 This file was only used during ocamldebug sessions (in the dev/db
 script). It was containing a large subset of the core cma files,
 up to the printing functions. There were a few notable exceptions,
 for instance no kernel/vm.cmo to avoid loading dllcoqrun.so in ocamldebug.
 But printers.cma was troublesome to maintain : almost each time an ML file
 was added/removed/renamed in the core of Coq, dev/printers.mllib
 had to be edited, in addition to the directory-specific .mllib
 (kernel/kernel.mllib and co). So I propose here to kill this file,
 and put instead in dev/db several "load_printer" of the core cma files.

 For that to work, we need to compile kernel/kernel.cma with the right
 -dllib and -dllpath options, but that shouldn't hurt (on the contrary).
 We also source now the camlpX cma in dev/db, via a new generated file
 dev/camlp4.dbg containing a load_printer of either gramlib.cma or
 camp4lib.cma.

 If one doesn't want to perform the whole "source db" at the start
 of an ocamldebug session, then the former "load_printer printers.cma"
 could be replaced by:

  source core.dbg
  load_printer top_printers.cmo

 See for instance the minimal dev/base_db.
</pre>
</div>
</content>
</entry>
<entry>
<title>Printer</title>
<updated>2000-12-15T08:20:10+00:00</updated>
<author>
<name>mohring</name>
</author>
<published>2000-12-15T08:20:10+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=65febb705e4c76c24306a7dc30b8fe5902eefe13'/>
<id>65febb705e4c76c24306a7dc30b8fe5902eefe13</id>
<content type='text'>
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1117 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@1117 85f007b7-540e-0410-9357-904b9bb8a0f7
</pre>
</div>
</content>
</entry>
<entry>
<title>ajout constr_display</title>
<updated>2000-11-29T15:35:30+00:00</updated>
<author>
<name>filliatr</name>
</author>
<published>2000-11-29T15:35:30+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=378edbeede113c3bfdb9d2b46d5bfae19e96be65'/>
<id>378edbeede113c3bfdb9d2b46d5bfae19e96be65</id>
<content type='text'>
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1032 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@1032 85f007b7-540e-0410-9357-904b9bb8a0f7
</pre>
</div>
</content>
</entry>
<entry>
<title>rattrapage exceptions autres que UserError</title>
<updated>1999-12-14T13:49:42+00:00</updated>
<author>
<name>filliatr</name>
</author>
<published>1999-12-14T13:49:42+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=c8da19b11952126f09b9d32002534ce91ae0d47c'/>
<id>c8da19b11952126f09b9d32002534ce91ae0d47c</id>
<content type='text'>
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@254 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@254 85f007b7-540e-0410-9357-904b9bb8a0f7
</pre>
</div>
</content>
</entry>
<entry>
<title>pretty-printers pour le debugger</title>
<updated>1999-12-14T08:03:32+00:00</updated>
<author>
<name>filliatr</name>
</author>
<published>1999-12-14T08:03:32+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=e3be8cdf7c4aa3882028d460267b136dcc36754a'/>
<id>e3be8cdf7c4aa3882028d460267b136dcc36754a</id>
<content type='text'>
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@251 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@251 85f007b7-540e-0410-9357-904b9bb8a0f7
</pre>
</div>
</content>
</entry>
</feed>
