Re: [isabelle-dev] NEWS: formal comments

[Makarius Wenzel]

On 06.02.2018 17:31, Tobias Nipkow wrote:
This concerns only the inner syntax, where comments are rare. We should 
not give up the outer (* *) comments for something less convenient.


Informal outer comments are not going to disappear.

That means that users who don't have a formal meaning of comments in 
mind can remain unclear about it as before. (BTW, I often see outer 
comments in AFP articles that are actually meant as formal 'text' 
blocks, but apparently the authors never looked at the PDF output, where 
the informal comments are not shown at all -- just like % in LaTeX.)



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: formal comments

[Tobias Nipkow]

This concerns only the inner syntax, where comments are rare. We should not give 
up the outer (* *) comments for something less convenient.


Tobias

On 06/02/2018 15:13, Lawrence Paulson wrote:
Will there still be a way to comment out random junk? I often work with a 
mixture of Isabelle and commented-out HOL Light material.


Larry

On 26 Jan 2018, at 20:19, Makarius > wrote:


* Old-style inner comments (* ... *) within the term language are legacy
and will be discontinued soon: use formal comments "― ‹...›" or "⌦‹...›"
instead.




___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: formal comments

[Lawrence Paulson]

Will there still be a way to comment out random junk? I often work with a 
mixture of Isabelle and commented-out HOL Light material.

Larry

> On 26 Jan 2018, at 20:19, Makarius  wrote:
> 
> * Old-style inner comments (* ... *) within the term language are legacy
> and will be discontinued soon: use formal comments "― ‹...›" or "⌦‹...›"
> instead.

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Code check failed for SML on lxbroy10

[Fabian Immler]

Dear isabelle-dev,

I noticed that currently (isabelle:ed0a7090167d, AFP:26f074817c9a) 
AFP/Native_Word fails to build on lxbroy10 (with ML_system_64=true):
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype 
Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** At command "export_code" (line 889 of 
"~/work/afp/afp-devel/thys/Native_Word/Bits_Integer.thy")

The build works fine on e.g., lxbroy8. It also works on lxbroy10 with 
ML_system_64=false.

This is apparently since the introduction of polyml-5.7.1 
(isabelle:aefaaef29c58, AFP:c7180aa1cb8f).

Stripping the problem down, I realized that this has nothing to do with 
Native_Word, because the same issue arises with the following theory:

theory Test imports HOL.Code_Generator begin
export_code Code_Generator.holds checking SML
end

The log says:

Loading theory "Test.Test"
/home/immler/.isabelle/contrib/jdk-8u162/x86_64-linux/jre/bin/java: symbol 
lookup error: /usr/lib64/libhogweed.so.4: undefined symbol: __gmpn_cnd_add_n
### theory "Test.Test"
### 0.291s elapsed time, 0.009s cpu time, 0.000s GC time
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype 
Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** At command "export_code" (line 5 of "/mnt/home/immler/Test.thy")

Does anyone have an idea about this?
There seems to be an issue with the libraries on lxbroy10, but I wonder why 
this is only triggered with "export_code ... checking SML".

Best regards,
Fabian





smime.p7s
Description: S/MIME cryptographic signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] 25th Automated Reasoning Workshop (ARW 2018), University of Cambridge, 12-13 April 2018

[Dr A. Koutsoukou-Argyraki]

25th AUTOMATED REASONING WORKSHOP 2018

Cambridge, 12-13 April 2018
http://www.cl.cam.ac.uk/events/arw2018/

CALL FOR ABSTRACTS AND STUDENT TRAVEL GRANT APPLICATIONS

GENERAL INFORMATION

The 25th Automated Reasoning Workshop (ARW 2018) will take place at the 
University of Cambridge on 12-13 April 2018.


INVITED SPEAKERS

Ekaterina Komendantskaya (Heriot-Watt University)
Lawrence Paulson (University of Cambridge)

SCOPE

The workshop provides an informal forum for the automated reasoning 
community to discuss recent work, new ideas and applications, and 
current trends. It aims to bring together researchers from all areas of 
automated reasoning in order to foster links among researchers from 
various disciplines; among theoreticians, implementers and users alike.


Topics include but are not limited to:

- Theorem proving in classical and non-classical logics;
- Interactive theorem proving, logical frameworks, proof assistants, 
proof

  planning
- Reasoning methods:
* Saturation-based, instantiation-based, tableau, SAT
* Equational reasoning, unification
* Constraint satisfaction
* Decision procedures, SMT
* Combining reasoning systems
* Non-monotonic reasoning, commonsense reasoning
* Abduction, induction
* Model checking, model generation, explanation
- Formal methods to specifying, deriving, transforming and verifying 
computer systems, requirements and software

- Logic-based knowledge representation and reasoning:
* Ontology engineering and reasoning
* Domain specific reasoning (spatial, temporal, epistemic,agents, 
etc)

- Logic and functional programming, deductive databases
- Implementation issues and empirical results, demos
- Machine learning and automated reasoning systems
- Practical experience and applications of automated reasoning

The workshop will be highly interactive, giving all attendees an 
opportunity to participate. There will be sessions for displaying 
posters and open discussion sessions organised around specific topics 
such as "Automated Reasoning and Artificial Intelligence”.


SUBMISSIONS

We invite the submission of camera-ready, two-page extended abstracts 
about recent work, work in progress, or a system description.  The 
abstract can describe work that has already been published elsewhere. 
The main objective of the abstracts is to spread information about 
recent work in our community, and we expect to accept most on-topic 
submissions, but we may ask for revisions.


To prepare your submission, please use the ARW LaTeX style file provided 
from the workshop website. Each submission should include the names and 
complete addresses (including email) of all authors.  For the final 
versions we require all sources (TeX file and any input files).


Please send your submissions via EasyChair at 
https://easychair.org/conferences/?conf=arw2018. Correspondence will be 
sent to corresponding authors indicated on EasyChair.


PUBLICATION DETAILS

Abstracts will be published in informal workshop notes and will be made 
available on the workshop page. After the workshop we are hoping to 
solicit inaugural 25th anniversary of ARW articles for publication.


PRESENTATIONS

Each workshop participant will be asked to give a short talk (around 10 
minutes depending on time constraints) to introduce their research. Each 
participant will also be allocated space in a poster session (poster 
size up to A0), where they can further present and discuss their work. 
Please prepare posters for the event.


STUDENT GRANTS

We have a limited number of grants available to support PhD students in 
attending the event. If you are interested, please refer to the workshop 
website for details. The deadline to apply for student grants is 1 March 
2018.


IMPORTANT DATES

1 March 2018: Student grant application deadline
12 March 2018: Abstract submission
16 March 2018: Abstract, student grant notification
21 March 2018: Final version due, Registration deadline
12-13 April 2018: Workshop

PROGRAMME COMMITTEE

Alexander Bolotov Chair (University of Westminster)
Jacques Fleuriot Secretary/Treasurer (University of Edinburgh)
Simon Colton (Goldsmiths College, University of London)
Louise Dennis (University of Liverpool)
Ullrich Hustadt (University of Liverpool)
Mateja Jamnik (University of Cambridge)
Florian Kammueller (Middlesex University)
Ekaterina Komendantskaya (Heriot-Watt University)
Alice Miller (University of Glasgow)
Oliver Ray (University of Bristol)
Renate Schmidt (University of Manchester)

LOCAL ORGANISERS

Mateja Jamnik (Mateja dot Jamnik at cl dot cam dot ac dot uk)

Edward Ayers
Angeliki Koutsoukou-Argyraki
Wenda Li
Chaitanya Mangla
Lawrence Paulson
Zohreh Shams

CONTACT

arw2...@easychair.org
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev