Dear all,
we are past point 0 for the Isabelle2012 release. This means:
* http://isabelle.in.tum.de/repos/isabelle-release/rev/d9a09f965dab is
the starting point for the final phase before roll-out in > 2 weeks.
There is no push access. Any changes that are essential for the
rele
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 alre
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:
/home/griff/Downloads/Is
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 announc
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
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 wr
On 04/26/2012 03:01 PM, Makarius wrote:
On Thu, 26 Apr 2012, 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
On Thu, 26 Apr 2012, 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
button
On 04/26/2012 02:53 PM, Makarius wrote:
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.
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 x86_6
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, L
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
buttons
On 04/26/2012 02:31 PM, Ondřej Kunčar wrote:
On 04/26/2012 02:21 PM, Ondřej Kunčar wrote:
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
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 b
On 04/26/2012 02:21 PM, Ondřej Kunčar wrote:
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 sho
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.
Please
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.
Please report any problems with your exoti
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:
/home/griff/Downloads/Isabelle_25-Apr-2012/src/HOL/Mirabelle/Actions/mi
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
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: http://www4.in.tum.de/~wen
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
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, whic
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, which bundles both JDK and Cygwin 1.7.9, see the Downl
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 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 se
On Mon, 23 Apr 2012, Johannes Hölzl wrote:
The JDK in Isabelle_23-Apr-2012_bundle_x86-linux.tar.gz seams to be the
64-bit version:
Isabelle_23-Apr-2012/contrib/jdk-7u3_x86-linux/jdk1.7.0_03/bin/java: ELF
64-bit LSB executable, x86-64, version 1 (SYSV), dynamically linked
(uses shared libs),
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
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, becaus
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.
B
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.
Both changes do not change any ML files, and there
In preparation of the release, the following test website is now
available: http://www4.in.tum.de/~wenzelm/test/website/
So far this is just for warming up, and to see pending issues of overall
system integration. I have already updated many of the contributing
components: Scala, Java, Emacs,
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 accom
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 pl
Dear all,
the release is alreay in place, but before announcing it officially the
Sydney mirror needs another round of updating, which will probably happen
around midnight GMT. This gives another chance to sport drop-outs on the
website.
The main Isabelle repository is already in post-relea
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 t
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
http://isabelle.in.tum.de/reports/Isabel
The release branch for Isabelle2011-1 is now at
http://isabelle.in.tum.de/repos/isabelle-release
Any small changes and amendments can be mailed to me (cf. "hg export" or
"hg bundle"). Things to be added to isabelle-release should *not* be
pushed on the main isabelle repository, to avoid the c
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 Sat, 24 Sep 2011, Makarius wrote:
Here is another pre-release snapshot:
http://www4.in.tum.de/~wenzelm/test/Isabelle_24-Sep-2011
This is probably the last one before the final release phase starts within
the next few days. This means:
* The isabelle repository is cloned to isabelle-rel
On 01/07/2011 11:56 PM, Gerwin Klein wrote:
On 07/01/2011, at 11:59 PM, Makarius wrote:
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 wou
On 07/01/2011, at 11:59 PM, Makarius wrote:
> 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
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,
C
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 d
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 G
On Fri, 7 Jan 2011, Lawrence Paulson wrote:
I'm afraid that I originated the custom of not always linking the
release name to the calendar year. The idea was to indicate that the new
release consisted of little more than patches from the previous one. So,
one option is to call it Isabelle 2009
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
Hi all,
> Year numbers are very comfortable.
That's true, with the disadvantage that there fits only one year in a
year, and I have the impression that the recent naming discussions were
mainly influenced by the motivation to keep the current year number free
for the last release of a year.
In m
I think the yearly naming convention has a rustic charm about it, kind
of like french wines. We can all sit down one day and have a big
discussion which year was the best vintage. Reminisce about the more
intense full-bodied flavour of the second batch of 2009, which is lovely
in small sips, bu
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 us
On 07/01/2011, at 8:00 PM, Michael Norrish wrote:
> On 7/01/11 7:53 PM, Tobias Nipkow wrote:
>> I don't see any good reason for the skewed naming scheme of 2009-x in
>> 2010 or 2011. We should use the year that the release was made in,
>> period. That avoids unproductie arguments on how major or m
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
On 7/01/11 7:53 PM, Tobias Nipkow wrote:
I don't see any good reason for the skewed naming scheme of 2009-x in
2010 or 2011. We should use the year that the release was made in,
period. That avoids unproductie arguments on how major or minor a
release is.
Or dispense with year numbers entirely.
I don't see any good reason for the skewed naming scheme of 2009-x in
2010 or 2011. We should use the year that the release was made in,
period. That avoids unproductie arguments on how major or minor a
release is.
I guess my email is a case of "everything has been said already but not
yet by ever
I'm afraid that I originated the custom of not always linking the release name
to the calendar year. The idea was to indicate that the new release consisted
of little more than patches from the previous one. So, one option is to call it
Isabelle 2009-3, which would mean that it is still essentia
On Thu, Jan 6, 2011 at 8:59 AM, Makarius 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
> "Isabelle2010"
I think a release date of January 2011 still justifies to call the
release "Isabelle2010".
Why would we want to, though?
I suppose Makarius suggested this to be able to call the release due
at the end of the year 2011 rather than 2011-1.
Not that it's that important (which makes it all th
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 e
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 manages to wrap up until the beginning of next week,
Dear isabelle-dev,
Since we now have this nice new Isabelle release, I thought it would
be nice to have a little release party. So I invite all Isabelle
contributors/power users who happen to be in reachable distance to a
slightly spontaneous
ISABELLE 2009-1 RELEASE PARTY
S
After additional delays due to some confusion how the release process
actually works, we have now reached point zero. This means that version
2ca2693a8c10 has been forked to a separate repository clone
http://isabelle.in.tum.de/repos/isabelle-release
This is meant to become the officially p
On Wed, 18 Nov 2009, Makarius wrote:
> On Fri, 16 Oct 2009, Makarius wrote:
>
>> Dear Isabelle contributors,
>>
>> we need to approach the next official Isabelle release. The basic plan is
>> to get things done this fall, which means there are only 2-3 weeks left for
>> substantial changes. A
On Fri, 16 Oct 2009, Makarius wrote:
> Dear Isabelle contributors,
>
> we need to approach the next official Isabelle release. The basic plan
> is to get things done this fall, which means there are only 2-3 weeks
> left for substantial changes. After that there will be a few more weeks
> for
I have some long-planned changes to the HOLCF domain package that are
now nearly complete; since there are some users waiting on some
upcoming features, it would be a shame for them to have to wait
another release cycle.
I will require more than just a few days, though. Probably if I work
hard I c
Dear Isabelle contributors,
we need to approach the next official Isabelle release. The basic plan is
to get things done this fall, which means there are only 2-3 weeks left
for substantial changes. After that there will be a few more weeks for
polishing and fine-tuning -- this phase becomes
See http://www4.in.tum.de/~wenzelm/test/website-test/ for the latest test
version, which is unlikely to change again for the final release.
The precompiled binaries are now for Poly/ML 5.2, which has been released
just today. Moreover, there are now logic images for Cygwin, and more
explicit i
This is just a reminder that the time for non-essential changes to ML and
thy sources has already run out last week!
There are still a few days to work on the manuals -- without changing the
main theory sources of the underlying library, though.
Makarius
See http://www4.in.tum.de/~wenzelm/test/website-test/ for a test version
of the forthcoming release, including the usual precompiled binaries
(still for Poly/ML 5.1).
Makarius
Dear Isabelle contributors,
the code freezing time for Isabelle2008 is imminent. Any last minute
commits should be restricted to real show stoppers. There are still a
couple of days to tune documentation, though. Please also check your
entries in NEWS and CONTRIBUTORS.
Makarius
68 matches
Mail list logo
