On Thu, 26 Apr 2012, Christian Sternagel wrote:
Referring to
http://www4.in.tum.de/~wenzelm/test/website/dist/Isabelle_25-Apr-2012_bundle_x86_64-linux.tar.gz
When calling
./bin/isabelle mirabelle
I obtain
...
Available OPTIONs for the ACTION sledgehammer:
grep:
Am 02.05.2012 um 13:55 schrieb Makarius:
On Thu, 26 Apr 2012, Christian Sternagel wrote:
I was just curious what mirabelle actually is/does, which I still don't
know.
I don't know how (or if) it is tested.
The HOL-Mirabelle session ensures that the ML code compiles. This already
This is probably the last update of the test website
http://www4.in.tum.de/~wenzelm/test/website/ before official release
candidates for Isabelle2012 will be announced (also on isabelle-users).
The current plan for the deadline for point 0 (the repository fork) is
02-May-2012 -- I will
On 04/26/2012 02:09 PM, Makarius wrote:
The website itself is starting to take shape. Thanks to Johannes Hölzl
we now have nice download buttons that detect the platform of the web
browser: Linux, Linux 64 bit, Mac OS X, Windows. All 4 buttons are shown
if the platform cannot be detected.
On Thu, 2012-04-26 at 14:09 +0200, Makarius wrote:
The website itself is starting to take shape. Thanks to Johannes
Hölzl we now have nice download buttons that detect the platform of
the web browser: Linux, Linux 64 bit, Mac OS X, Windows. All 4
buttons are shown if the platform cannot be
On 26.04.2012 14:32, Tjark Weber wrote:
On Thu, 2012-04-26 at 14:09 +0200, Makarius wrote:
The website itself is starting to take shape. Thanks to Johannes
Hölzl we now have nice download buttons that detect the platform of
the web browser: Linux, Linux 64 bit, Mac OS X, Windows. All 4
On Thu, 26 Apr 2012, Lars Noschinski wrote:
On 26.04.2012 14:32, Tjark Weber wrote:
On Thu, 2012-04-26 at 14:09 +0200, Makarius wrote:
The website itself is starting to take shape. Thanks to Johannes
Hölzl we now have nice download buttons that detect the platform of
the web browser: Linux,
On Thu, 26 Apr 2012, Ondřej Kunčar wrote:
My operating system is detected as 32-bit Linux for the following user
agent strings, which is wrong.
Mozilla/5.0 (X11; Linux x86_64) AppleWebKit/536.4 (KHTML, like Gecko)
Chrome/19.0.1079.0 Safari/536.4 SUSE/19.0.1079.0
Opera/9.80 (X11; Linux
It works for me, and the auto-detect is nice.
The option to download for arbitrary platforms is occasionally useful, but
isn't worth making a big effort. A simple link or button labelled “other
platforms or “show all platforms should be sufficient.
Larry
On 26 Apr 2012, at 13:09, Makarius
The current state of the Download-button can be seen here:
http://www21.in.tum.de/~hoelzl/test/
* If the detection does not work all platforms are shown as button
* If the detection works then the suggested platforms are shown as
buttons, and the other ones as normal links
- Johannes
Hi all,
I spotted this strange line in the NEWS (linked from the test website)
symp_def ~ (dropped, use symp_def and sym_def instead)
cheers
chris
On 04/18/2012 10:18 PM, Makarius wrote:
In preparation of the release, the following test website is now
available:
Referring to
http://www4.in.tum.de/~wenzelm/test/website/dist/Isabelle_25-Apr-2012_bundle_x86_64-linux.tar.gz
When calling
./bin/isabelle mirabelle
I obtain
...
Available OPTIONs for the ACTION sledgehammer:
grep:
On Tue, 24 Apr 2012, Jasmin Christian Blanchette wrote:
Am 23.04.2012 um 17:22 schrieb Makarius:
Here is an update of the test website for warming up a bit more
http://www4.in.tum.de/~wenzelm/test/website/
I've spent this cold and wet weekend to produce a monolitic Windows
application,
Hi Makarius,
I suppose here that the self-extracting Isabelle_23-Apr-2012.exe archive did
extract correctly, to something like 850 MB directory structure?
At least it had the expected directory structure.
Your existing Cygwin is probably relatively old, such that the poly.exe
cannot be
Here is an update of the test website for warming up a bit more
http://www4.in.tum.de/~wenzelm/test/website/
I've spent this cold and wet weekend to produce a monolitic Windows
application, which bundles both JDK and Cygwin 1.7.9, see the Download
page. (Cygwin 1.7.9 is important here,
Am Montag, den 23.04.2012, 17:22 +0200 schrieb Makarius:
Here is an update of the test website for warming up a bit more
http://www4.in.tum.de/~wenzelm/test/website/
I've spent this cold and wet weekend to produce a monolitic Windows
application, which bundles both JDK and Cygwin 1.7.9,
On 04/23/2012 05:22 PM, Makarius wrote:
Here is an update of the test website for warming up a bit more
http://www4.in.tum.de/~wenzelm/test/website/
From the monolithic Windows App (with Windows 7):
The font in the little symbol replacement popup seems to be wrong: When
I enter ==, I just
On Mon, 23 Apr 2012, Alexander Krauss wrote:
On 04/23/2012 05:22 PM, Makarius wrote:
Here is an update of the test website for warming up a bit more
http://www4.in.tum.de/~wenzelm/test/website/
From the monolithic Windows App (with Windows 7):
The font in the little symbol replacement popup
On Wed, 18 Apr 2012, Johannes Hölzl wrote:
When the testboard gives me green light I will tomorrow also push a
reworked Probability theory which only takes 2 min to build instead of 5
min as before. I also want to push a new version of the Floats which
uses the new lifting infrastructure.
I looked for the documentation of HOL-Probability, but it looks like it is
missing. It should be under HOL-Multivatiate-Analysis, but there are now
further Session. Was there a change in the build-system?
- Johannes
On Mon, 10 Oct 2011, Makarius wrote:
Dear all,
the release is alreay in
On Mon, 10 Oct 2011, Johannes Hoelzl wrote:
I looked for the documentation of HOL-Probability, but it looks like it is
missing. It should be under HOL-Multivatiate-Analysis, but there are now
further Session. Was there a change in the build-system?
Yes in fc3bb3a42369 by Alex Krauss, to
Am 26.09.2011 um 20:20 schrieb Makarius:
I am about to produce the release clone. The current tip eb7a797ade0f will
probably be the fork point. This includes a few changes by Lukas and Jasmin
from today, and I understand that these were meant to go into this release,
not the next one.
On 09/26/2011 11:38 PM, Makarius wrote:
isatest will also test http://isabelle.in.tum.de/repos/isabelle-release
within the next few weeks. (In the past I used to have a minimal isatest
for http://isabelle.in.tum.de/repos/isabelle but that was superseded by
On 27/09/2011, at 7:45 AM, Alexander Krauss wrote:
On 09/26/2011 11:38 PM, Makarius wrote:
isatest will also test http://isabelle.in.tum.de/repos/isabelle-release
within the next few weeks. (In the past I used to have a minimal isatest
for http://isabelle.in.tum.de/repos/isabelle but that
Hi all,
(must add my 2ct, too)
Concerning the content of the next release:
Brian wrote:
What exactly makes it major? Judging by the NEWS file, it looks
like 2009-2 introduced about as many new features as the upcoming
release will. Is there any new feature in particular that is
considered a
On 7/01/11 8:05 PM, Alexander Krauss wrote:
But then we need a Marketing division to come up with a new name every 8
months :-}. Year numbers are very comfortable.
You either come up with a set of names to use, or just do what most
software projects do (commercial and open source both), and
I like the wine connection! Not just French wines, but also Australian
ones, and German Rieslings come to mind. Not sure though how the UK fits
in, at least not yet, although global warming will fix that in a few
decades.
Tobias
Rafal Kolanski schrieb:
I think the yearly naming convention has
I'm afraid that English wine production has been increasing year by year. Some
of them are even said to be good.
http://www.english-wine.com/vineyards.html
Larry
On 7 Jan 2011, at 09:30, Tobias Nipkow wrote:
I like the wine connection! Not just French wines, but also Australian
ones, and
On 07/01/11 20:07, Michael Norrish wrote:
On 7/01/11 8:05 PM, Alexander Krauss wrote:
But then we need a Marketing division to come up with a new name every 8
months :-}. Year numbers are very comfortable.
You either come up with a set of names to use, or just do what most
software projects
On Fri, 7 Jan 2011, Rafal Kolanski wrote:
Taking a page from a successful marketing campaign, we could also adopt
a variation on the Ubuntu way of naming things, two numbers: year and
month. So this would be Isabelle 10.01.
We can even add silly names like Anomalous Assumption, Bound Beta,
On 07/01/2011, at 3:59 AM, Makarius wrote:
Bonne année à tous,
this is a reminder that we are approaching the next official Isabelle
release. I've got myself caught into too many other tasks over Christmas
vacation, and will now see how quick we can get a lift off.
If everybody else
On Thu, Jan 6, 2011 at 8:59 AM, Makarius makar...@sketis.net wrote:
If everybody else manages to wrap up until the beginning of next week, we
have a good chance to release before the end of the month.
This sounds good.
I think a release date of January 2011 still justifies to call the release
32 matches
Mail list logo
