Isabelle comment syntax

[larsrh]

The (* ... *) syntax for comments has been deprecated in Isabelle2018 and now finally been removed.

There's a syntax that works both for Isabelle2018 and recent development versions:

\<comment> \<open> ... \<close>

Unfortunately, everything in these comments are processed by the TeX output of Isabelle. Some symbols require additional escaping. Here's a diff that should highlight the problem:

--- a/thys/CakeML/generated/Lem_num.thy Sun Sep 23 20:59:33 2018 +0200
+++ b/thys/CakeML/generated/Lem_num.thy Sun Sep 23 21:31:49 2018 +0200
@@ -264,7 +264,7 @@
 fun  gen_pow_aux  :: "('a \<Rightarrow> 'a \<Rightarrow> 'a)\<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a "  where 
      " gen_pow_aux (mul :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) (a :: 'a) (b :: 'a) (e :: nat) = (
    (case  e of
-       0 => a (* cannot happen, call discipline guarentees e >= 1 *)
+       0 => a \<comment> \<open>cannot happen, call discipline guarentees \<open>e >= 1\<close>\<close>
      | (Suc 0) => mul a b
      | (  (Suc(Suc e'))) => (let e'' = (e div( 2 :: nat)) in
                    (let a' = (if (e mod( 2 :: nat)) =( 0 :: nat) then a else mul a b) in

A solution that would always work would be to escape everything in a comment.

I'd be happy to take a stab at implementing this, but so far I haven't been able to figure out how and where comment printing works in Lem.

[larsrh]

I forgot the other obvious solution: Drop comments. I'm tempted to implement that in my fork just to make it work. Still, this requires me to understand comment printing.

[PeterSewell]

Comments are special cases of interstitial things (constructor Inter), containing Ast.Com. In backend.ml, for Isabelle:

module Isa () : Target = struct include Identity

let lex_skip = function | Ast.Com(r) -> Ulib.Text.filter (fun c -> not(c = quotation_mark) && not (c=backslash)) (ml_comment_to_rope r) | Ast.Ws(r) -> r | Ast.Nl -> r"\n"

But you should also look at the tex-specific path to_rope_tex_single, in output.ml.

Try not to escape more than necessary, to avoid hopelessly noisy output.

thanks, Peter

On 24 September 2018 at 07:43, Lars Hupel notifications@github.com wrote:

The ( ... ) syntax for comments has been deprecated in Isabelle2018 and now finally been removed.

There's a syntax that works both for Isabelle2018 and recent development versions:

\ \ ... \

Unfortunately, everything in these comments are processed by the TeX output of Isabelle. Some symbols require additional escaping. Here's a diff that should highlight the problem:

--- a/thys/CakeML/generated/Lem_num.thy Sun Sep 23 20:59:33 2018 +0200+++ b/thys/CakeML/generated/Lem_num.thy Sun Sep 23 21:31:49 2018 +0200@@ -264,7 +264,7 @@ fun gen_pow_aux :: "('a \ 'a \ 'a)\ 'a \ 'a \ nat \ 'a " where " gen_pow_aux (mul :: 'a \ 'a \ 'a) (a :: 'a) (b :: 'a) (e :: nat) = ( (case e of- 0 => a ( cannot happen, call discipline guarentees e >= 1 )+ 0 => a \ \cannot happen, call discipline guarentees \e >= 1\\ | (Suc 0) => mul a b | ( (Suc(Suc e'))) => (let e'' = (e div( 2 :: nat)) in (let a' = (if (e mod( 2 :: nat)) =( 0 :: nat) then a else mul a b) in

A solution that would always work would be to escape everything in a comment.

I'd be happy to take a stab at implementing this, but so far I haven't been able to figure out how and where comment printing works in Lem.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/rems-project/lem/issues/20, or mute the thread https://github.com/notifications/unsubscribe-auth/AErM5s8OCaBcAL5HukPaKS7TqBnUOmFdks5ueH8ZgaJpZM4W2IP- .

[bauereiss]

ee63710d751e7a359cc7c0f8ac33c4c16a12f181 seems to work for the Lem files of Sail and its models, except for one case where a backslash occurs in a comment inside a function definition (the same comment seems to work fine outside the function). But I don't think it's worth trying to handle that in Lem; I'll just remove that comment from Sail.