Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

[Florian Haftmann]

>> Are there any issues remaining on this thread after
>> http://isabelle.in.tum.de/repos/isabelle/rev/55534affe445 ?
> 
> I get this failure on my regular Ubuntu 18.04:
> 
> *** Failed to load theory "HOL-Library.Library" (unresolved
> "HOL-Library.Finite_Map")
> *** Code check failed for OCaml: "$ISABELLE_ROOT/lib/scripts/ocamlexec"
> ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml
> *** At command "export_code" (line 1428 of
> "~~/src/HOL/Library/Finite_Map.thy")
> 
> 
> ocamlexec appears to reconfigure the OPAM installation insided
> Isabelle/ML, but this is conceptually wrong as I explained already.

I would doubt that since ocamlexec is modelled following the existing
scripts ocamlc and ocaml; the only candidates for irregular activities
would be ocamlfind and ocamlopt themselves, which would be strange.

> Also note that ISABELLE_OPAM_ROOT is always provided, even it that is
> not active.

OK, this might at least explain the reproducible failure above.

Let's see what we get after the next iteration.

Cheers,
Florian



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

Re: [isabelle-dev] [Isabelle-ci] Build failure in Isabelle+AFP (slow)

[Florian Haftmann]

I'm note sure what's going on here.

It appears to be a spontaneous dropout of the OCaml environment,
sporadically: in session Native_Word, theory
~~/afp/thys/Native_Word/Bits_Integer.thy seems to success, whereas in
e.g. Iptables_Semantics it fails.

I did not experience anything like that on lxcisa0 with -j 6 and the
latest polyml 5.8 rc (!).

  ML_PLATFORM="x86_64_32-linux"
  ML_OPTIONS="--minheap 500"

Are there any other clues to have a look for?

Cheers,
Florian

Am 14.03.19 um 12:38 schrieb Isabelle/Jenkins:
> Iptables_Semantics FAILED
> (see also 
> /media/data/jenkins/workspace/isabelle-nightly-slow/heaps/polyml-5.8_x86_64-linux/log/Iptables_Semantics)
> Loading theory "Iptables_Semantics.Semantics_Embeddings"
> ### theory "Iptables_Semantics.Semantics_Embeddings"
> ### 1.148s elapsed time, 8.876s cpu time, 0.168s GC time
> Loading theory "Iptables_Semantics.Access_Matrix_Embeddings"
> Loading theory "Iptables_Semantics.Iptables_Semantics"
> ### theory "Iptables_Semantics.Iptables_Semantics"
> ### 0.078s elapsed time, 0.616s cpu time, 0.000s GC time
> Loading theory "Iptables_Semantics.No_Spoof_Embeddings"
> "False"
>   :: "bool"
> ### theory "Iptables_Semantics.No_Spoof_Embeddings"
> ### 0.192s elapsed time, 1.524s cpu time, 0.000s GC time
> ### theory "Iptables_Semantics.Access_Matrix_Embeddings"
> ### 0.966s elapsed time, 6.944s cpu time, 0.300s GC time
> (\r m.
> \r \ set ?rs; ?f (get_match r) = Some m\
> \ normalized_nnf_match m \
>   \ has_disc_negated disc3 False m \
>   P m) \
> \r\set (optimize_matches_option ?f ?rs).
>normalized_nnf_match (get_match r) \
>\ has_disc_negated disc3 False (get_match r) \ P (get_match r)
> \\r\set ?rs.
> normalized_nnf_match (get_match r) \
> \ has_disc_negated disc3 False (get_match r);
>  \m.
> normalized_nnf_match m \
> \ has_disc_negated disc3 False m \
> (\m'\set (?f m). ?Q m')\
> \ \r\set (normalize_rules ?f ?rs).
>  ?Q (get_match r)
> isabelle document -d 
> /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics/document
>  -o pdf -n document
> isabelle document -d 
> /media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics/outline
>  -o pdf -n outline -t /proof,/ML
> *** Failed to load theory "Native_Word.Code_Target_Bits_Int" (unresolved 
> "Native_Word.Bits_Integer")
> *** Failed to load theory "Iptables_Semantics.Code_Interface" (unresolved 
> "Native_Word.Code_Target_Bits_Int")
> *** Failed to load theory "Iptables_Semantics.Parser" (unresolved 
> "Iptables_Semantics.Code_Interface")
> *** Failed to load theory "Iptables_Semantics.Code_haskell" (unresolved 
> "Iptables_Semantics.Parser")
> *** Failed to load theory "Iptables_Semantics.Documentation" (unresolved 
> "Iptables_Semantics.Code_Interface")
> *** Code check failed for OCaml: "$ISABELLE_ROOT/lib/scripts/ocamlexec" 
> ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml
> *** At command "export_code" (line 630 of 
> "~~/afp/thys/Native_Word/Bits_Integer.thy")
> Iptables_Semantics_Examples CANCELLED
> Iptables_Semantics_Examples_Big CANCELLED
> Unfinished session(s): ConcurrentGC, ConcurrentIMP, HOL-Library, 
> Iptables_Semantics, Iptables_Semantics_Examples, 
> Iptables_Semantics_Examples_Big, JinjaThreads



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

Re: [isabelle-dev] NEWS

[Florian Haftmann]

Am 13.03.19 um 20:57 schrieb Lars Hupel:
>>   isabelle ocaml_opam install zarith
> 
> This should ideally happen on-the-fly from within Isabelle/ML.

Or maybe as implicit part  of

isabelle ocaml_setup

?

Florian



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

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

[Florian Haftmann]

Are there any issues remaining on this thread after
http://isabelle.in.tum.de/repos/isabelle/rev/55534affe445 ?

Cheers,
Florian

Am 24.06.18 um 22:29 schrieb Makarius:
> On 07/06/18 15:22, Lars Hupel wrote:
>>> Does this minimal approach make any sense, and solve the imminent
>>> administrative problems? In particular without a decision yet about
>>> ISABELLE_OCAML_VERSION vs. ISABELLE_OCAML / ISABELLE_OCAMLC?
>>
>> I tend to agree. Let's fix OCaml to 4.05.0 and we can figure out a good
>> way to upgrade after the release.
> 
> (This thread is still open.)
> 
> I presently tend to postpone the question if/how to support OCaml after
> the Isabelle2018.
> 
> 
>   Makarius
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 



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

[isabelle-dev] Current AFP problems

[Florian Haftmann]

isabelle: 03bc14eab432 tip
afp: 16e89cda027a tip

> Smooth_Manifolds FAILED
> (see also 
> /home/haftmann/data/tum/isabelle/master/heaps/polyml-5.8_x86_64_32-linux/log/Smooth_Manifolds)
> ### \finite ?S; \T\?S. closed T\
> ### \ closed (\ ?S)
> ### Rule already declared as introduction (intro)
> ### \finite ?A; \x\?A. closed (?B x)\
> ### \ closed (\ (?B ` ?A))
> ### Rule already declared as introduction (intro)
> ### \open ?S; closed ?T\ \ open (?S - ?T)
> ### Rule already declared as introduction (intro)
> ### \closed ?S; open ?T\ \ closed (?S - ?T)
> ### Rule already declared as introduction (intro)
> ### closed ?S \ open (- ?S)
> ### Rule already declared as introduction (intro)
> ### open ?S \ closed (- ?S)
> ### Rule already declared as introduction (intro)
> ### continuous_on ?s (linepath ?a ?b)
> ### Rule already declared as introduction (intro)
> ### (\i. continuous_on UNIV (\x. ?f x i)) \
> ### continuous_on UNIV ?f
> \\x.
> x \ manifold_eucl.diff_fun_space k \
> X x \ UNIV;
>  \x.
> x \ ?S \
> ?g x \ manifold_eucl.diff_fun_space k\
> \ X (\x. \i\?S. ?g i x) =
>   (\a\?S. X (?g a))
> locale diff
>   fixes k :: "enat"
> and charts1 :: "('a, 'e) chart set"
> and charts2 :: "('b, 'f) chart set"
> and f :: "'a \ 'b"
>   assumes "diff k charts1 charts2 f"
> locale c_manifold
>   fixes charts :: "('a, 'b) chart set"
> and k :: "enat"
>   assumes "c_manifold charts k"
> ### theory "Smooth_Manifolds.Cotangent_Space"
> ### 2.370s elapsed time, 12.536s cpu time, 4.080s GC time
> *** Failed to refine any pending goal
> *** At command "by" (line 632 of "$AFP/Smooth_Manifolds/Analysis_More.thy")
> 
> Finished HOL-Probability (0:01:16 elapsed time, 0:06:44 cpu time, factor 5.26)
> Building Randomised_Social_Choice ...
> Randomised_Social_Choice FAILED
> (see also 
> /home/haftmann/data/tum/isabelle/master/heaps/polyml-5.8_x86_64_32-linux/log/Randomised_Social_Choice)
>Proof.context -> Proof.state
> val parse_rat = fn: Token.T list -> Rat.rat * Token.T list
> val parse_support = fn: string list parser
> val parse_lottery = fn: (string * Rat.rat) list parser
> val pref_classes = fn: 'a list list -> 'a list list
> val combine_all = fn: ('a * 'a -> 'b) -> 'a list -> 'b list
> val prepare_strategyproofness_intro_thms = fn:
>Proof.context ->
>  int option ->
>thm -> Preference_Profiles_Cmd.info list -> (binding * thm list) list
> val gen_derive_strategyproofness_conditions = fn:
>Proof.context -> int option -> thm option -> term list -> Proof.state
> val derive_strategyproofness_conditions_cmd = fn:
>int option -> thm option -> string list -> Proof.context -> Proof.state
> ### theory "Randomised_Social_Choice.SDS_Automation"
> ### 2.607s elapsed time, 12.148s cpu time, 1.084s GC time
> ### Ignoring duplicate rewrite rule:
> ### mset (map ?f1 ?xs1) \ image_mset ?f1 (mset ?xs1)
> *** Failed to finish proof (line 462 of 
> "$AFP/Randomised_Social_Choice/Stochastic_Dominance.thy"):
> *** goal (1 subgoal):
> ***  1. \(\a | a \ carrier \ le x a. pmf p a) +
> ***  (\a\carrier.
> *** \ *
> *** (pmf p a * real (length xs - weak_ranking_index a)))
> ***  \ (\a | a \ carrier \ le x a. pmf q a) +
> ***(\a\carrier.
> ***   \ *
> ***   (pmf q a * real (length xs - weak_ranking_index 
> a)));
> ***  x \ carrier; {y. le x y} \ carrier\
> *** \ (\y | le x y. pmf p y) +
> ***   (\n\carrier.
> ***  \ *
> ***  (pmf p n *
> ***   real (length xs - weak_ranking_index n)))
> ***   \ (\y | le x y. pmf q y) +
> *** (\n\carrier.
> ***\ *
> ***(pmf q n *
> *** real (length xs - weak_ranking_index n)))
> *** At command "by" (line 462 of 
> "$AFP/Randomised_Social_Choice/Stochastic_Dominance.thy")
> SDS_Impossibility CANCELLED
> Unfinished session(s): Randomised_Social_Choice, SDS_Impossibility, 
> Smooth_Manifolds
> 0:10:29 elapsed time, 0:49:07 cpu time, factor 4.68

Cheers,
Florian




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

[isabelle-dev] Specification packages in Isabelle/HOL, particularly primrec

[Florian Haftmann]

Hi all,

after 3bfa28b3a5b2  (followed-up by AFP  d058960a13d6) the matter of
affairs with specification packages is as as follows:

The prototypical specification interface is of shape

  val add_specification: spec -> local_theory -> result * local_theory

where »spec« is the input specification and »result« a characterization
of the definitional extension with enough information to build on it in
derived tools.

The corresponding package is supposed to provide a morphism lifter for
results

  val transform: morphism -> result -> result

The local theory stemming from add_specification may still contain
hypothetical results of the specification construction (I left this
untouched contrary to an idea I have expressed earlier on this
mailinglist); to get a proper close-up, there is a set of combinators:

* Local_Theory.subtarget_result for regular nested local theory;
* Named_Target.theory_map_result for global specifications;
* Overloading.theory_map_result for global overloaded specifications;
* Class.theory_map_result for global overloaded specifications relating
to type class instantiation.

Hence various *_global variants for specification packages have been
removed.

What I have left untouched are the various variants of primrec. Is there
still an ongoing work or plan to get rid of the old datatype / primrec
layer, or at least to have that retreat further? Otherwise I would have
a closer look a it to get an idea what can be done there.

Cheers,
Florian



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

Re: [isabelle-dev] Timeouts in Flyspeck_Tame

[Florian Haftmann]

Am 14.02.19 um 13:34 schrieb Makarius:
> On 14/02/2019 12:04, Florian Haftmann wrote:
>>>> At the moment I am thinking whether the old approach of checking
>>>> everything except the computations can be restored without using fancy
>>>> low-level stuff.  Maybe by a locale.
>>>
>>> This is indeed a bit fragile. I used to make manual tests of
>>> Flyspeck-Tame over some time, but now ignore that problem.
>>>
>>> Maybe it is possible to make a non-slow session "Flyspeck-Tame-Base"
>>> that does everything except the actual "eval" steps, and postpone the
>>> checks to session Flyspeck-Tame (very_slow) = Flyspeck-Tame-Base ...
>>
>> Something like that indeed.  A completeness proof relative to a locale
>> which has the computational results as assumption apt for later
>> interpretation.
> 
> In contrast to my proposal concerning Flyspeck-Tame-Base it is better to
> keep the main AFP document unchanged, e.g. like this:
> 
>   session Flyspeck-Tame-Eval (very_slow) = Flyspeck-Tame + ...
> 
> This will change the timing for Flyspeck-Tame in the recorded database,
> but such renamings occasionally happen over the years.

See now
https://bitbucket.org/isa-afp/afp-devel/commits/00b771f6c60d99745fb933d4043c1ed123a427e5

Florian



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

Re: [isabelle-dev] Timeouts in Flyspeck_Tame

[Florian Haftmann]

>> At the moment I am thinking whether the old approach of checking
>> everything except the computations can be restored without using fancy
>> low-level stuff.  Maybe by a locale.
> 
> This is indeed a bit fragile. I used to make manual tests of
> Flyspeck-Tame over some time, but now ignore that problem.
> 
> Maybe it is possible to make a non-slow session "Flyspeck-Tame-Base"
> that does everything except the actual "eval" steps, and postpone the
> checks to session Flyspeck-Tame (very_slow) = Flyspeck-Tame-Base ...

Something like that indeed.  A completeness proof relative to a locale
which has the computational results as assumption apt for later
interpretation.

Florian



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

Re: [isabelle-dev] Timeouts in Flyspeck_Tame

[Florian Haftmann]

Am 10.02.19 um 17:01 schrieb Makarius:
> On 04/02/2019 14:17, Makarius wrote:
>> On 04/02/2019 10:37, Lars Hupel wrote:
>>> Is this related to the latest Poly/ML changes? The "slow" job still runs
>>> on the x86_64 platform. Last time it worked was 76fbd806ebc5. Hardware
>>> is 8-core LRZ VM.
>>
>> I can confirm this: see
>> https://isabelle.sketis.net/devel/build_status/AFP_bulky_64bit_6_threads/index.html
>>
>> I have switched back to stable polyml-5.7.1-8 for now (see
>> Isabelle/a5732629cc46) and will be unavailable for the next few days.
> 
> This did not change the non-termination, but the following helps:
> 
> changeset:   10116:9181c1974aa0
> tag: tip
> user:wenzelm
> date:Sun Feb 10 16:49:10 2019 +0100
> files:   thys/Flyspeck-Tame/PlaneGraphIso.thy
> description:
> adapted to Isabelle/7e4966eaf781 -- avoid non-termination;
> 
> I have merely applied the recommendation from the NEWS:
> 
>   INCOMPATIBILITY; consider using
>   declare image_cong_simp [cong del] in extreme situations.

Thanks for going into this.

But https://isabelle.sketis.net/devel/build_status/ still indicates
failure for Flyspec-Tame from Wed 13th.  Is there any chance that some
other non-termination proof requiring image_cong_simp [cong del] is
still left in Flyspeck-Tame?

Btw. that the ancient cond_eval hack has been replaced by a proper tag
has completely slipped out of my attention, hence I didn't notice that
Flyspeck-Tame is completely untested without very_slow.

At the moment I am thinking whether the old approach of checking
everything except the computations can be restored without using fancy
low-level stuff.  Maybe by a locale.

Cheers,
Florian



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

Re: [isabelle-dev] Analysis not building

[Florian Haftmann]

> HOL-Analysis can’t be built (reproducibly) with the latest version 
> (76f2d492627e). It simply dies, no error message.

I cannot reproduce this.

  ML_PLATFORM="x86_64_32-linux"
  ML_SYSTEM="polyml-5.7.1"
  ML_OPTIONS="--maxheap 9G"

Have you tried a fresh build or delete the corresponding log / saved
state manually?

Cheers,
Florian



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

Re: [isabelle-dev] NEWS: generated code as proper theory export

[Florian Haftmann]

>> Maybe the »checking« should just be a variant of the regular export.
>>
>> Hence the modification could be quite conservative:
>>
>>  export_code CONSTS in LANGUAGE ( '(' OPTIONS ')' ) ( module_name NAME )
>> ( file … | ( prefix … ) ( checked ) )
>>
>> where »file« denotes a relative root in the file system and »checked«
>> indicated that the generated code will be checked implicitly.
> 
> I have looked around at typical uses of 'export_code' in AFP. Most of
> the time it is just informative: writing a file and looking at it in the
> editor (or via the command-line!?), or doing that on the output channel.
> The isabelle-export: file-system covers that already, i.e. we should be
> able to eliminate almost all generated files from the AFP repository.
> 
> So "export_code .. file" should just disappear -- it is semantically
> illtyped in PIDE: editing the "file" argument will leave a trace of
> machine oil spilled to the physical file-system.
> 
> 
> We do need an explicit prefix and an internal check for duplicates, e.g.
> as in the command 'generated_file'.
> 
> That should be really just a prefix for the exported artifact, not the
> name itself: each language processor should be smart enough to derive
> file or directory names from it as required.  Thus the prefix locally
> belongs in front of the arguments.
> 
> Here is an example from AFP/160ac13cdc05
> SATSolverVerification/SatSolverCode.thy:
> 
>   export_code solve
> in OCaml file "code/solve.ML"
> in SML file "code/solve.ocaml
> in Haskell file "code/"
> 
> It could be turned into something like this:
> 
>   export_code "code/" = solve in OCaml SML Haskell
> 
> Some details about the automatic name derivation scheme still need to be
> sorted out -- or 'file' remains as an option to specify the suffix for
> effective name (without writing anything to the file-system).

Some further round of thinking.  Indeed, naming files is a little bit
delicate since there are two classes of target languages here: Haskell
with its strict one module – one file approach and ML where source code
is conceptually just a stream.  Hence in the current implementation the
exact interpretation of the »file« argument is up to the target language.

To make this more fitting, at the moment I am thinking about something like

> export_code [ ( NAME | PREFIX._ ) = ] CONSTS in LANGUAGE [ '(' OPTIONS ')' ] 
> [ file_prefix PATH ] [ checked ] 

* »checked« is just an aside to regular code generation, no distinctive
variant

* A mere prefix for the relative location can be given after »file_prefix«.

* Language-specific options remain as they are.

* The module naming schema gets more sophisticated: default, name or
prefix.  The key point is that this naming schema is again
target-language specific.

  For ML:
   code   file name
  default  multiple structurestheory name
  name one structure NAME NAME
  prefix   one structure PREFIX with multiple structures  PREFIX

  For Haskell:
   codefile name
  default  multiple modulesmodule name
  name one module NAME NAME
  prefix   multiple modules beneath PREFIX PREFIX module name

This should cover all application cases.

It will take further rounds of refinement to actually get there.

At the moment I am still in favour of a diagnostic command to emit sth
ad-hoc into the file system -- but this could be something separate from
export_code and maybe just use $ISABELLE_TMP_PREFIX/… as destination.

Just an aside: with the current tool support in Isabelle/jEdit I
consider the auxiliary construct »file ‹›« obsolete – the regular
exports are just two clicks away.

Cheers,
Florian



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

Re: [isabelle-dev] State of the art in Isabelle with OCaml, opam and zarith

[Florian Haftmann]

Hi Lars,

Am 22.01.19 um 22:34 schrieb Lars Hupel:
> It is admittedly a complicated incantation, but here you go:
> 
> $ cat test.ml
> let x = Z.one;;
> let _ = print_endline (Z.to_string x);;
> 
> $ isabelle ocaml_opam config exec ocamlfind -- ocamlopt -package zarith
> -linkpkg test.ml
> 
> $ ./a.out
> 1
> 
> You need "ocamlfind" to tell the OCaml compiler ("ocamlopt") where to
> look for packages.

thanks for that hint.

But ocamlfind semms not to provide a subcommand to invoke the
interactive OCaml toplevel.  What am I missing?

Cheers,
Florian



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

[isabelle-dev] Afterthoughts on Local_Theory.subtarget_result

[Florian Haftmann]

Hi all,

as of 82f57315cade (followed-up by AFP bf62184), the still occasionally
seen Local_Theory.reset invocations are gone, conveniently replaced by
Local_Theory.subtarget_result.

I'm considering pushing that even further: specification tools should by
contract provide a »clean« definitional extension without any artefacts
of the internal construction leaking out, i. e.

  val specification: spec -> local_theory -> result * local_theory

where »spec« is the input specification and »result« a characterization
of the definitional extension with enough information to build on it in
derived tools; the resulting local_theory can be continued on directly
-- all internal construction steps are hid in a local subtarget.

The corresponding package is supposed to provide a morphism lifter for
results

  val transform: morphism -> result -> result

hence exporting up through nested context is trivial.

This would also open up the possibility to get rid of the still seen
*_global variants for specification tools: using a combinator

  Named_Target.theory_map_result: (morphism -> 'a -> 'a) ->
(local_theory -> 'a * local_theory) -> theory -> 'a * theory

any Package.spec_global can be trivially inlined as

  Named_Target.theory_map_result Package.transform (Package.spec …)

So much my current understanding of affairs.

Cheers,
Florian









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

Re: [isabelle-dev] NEWS: generated code as proper theory export

[Florian Haftmann]

Hi Makarius,

>   * Are there remaining uses of 'file' with empty name? Is the virtual
> file-system browser sufficiently convenient to inspect results
> interactively?

I checked the file system browser and would be quite content with it; as
a bonus you can then make use of the syntax highlighting of jEdit (OCaml
seems not be built-in, though).

But I want to excite more feedback of users.

>   * How to specify proper (unique) export names: PIDE still lacks a
> check for uniqueness of export names, but overwriting existing exports
> is considered illegal. The 'file' allowed to produce separate names in
> the past, but it has a different meaning now (and is a candidate for
> deletion).

Well, if we re-consider the syntax, we will also find a way for this.

> Maybe 'export_code' should be renovated replaced by reformed commands
> like this:
> 
>   * "code_export PREFIX = CONSTS in LANGUAGE" where the PREFIX is
> optional and the default something like "generated" or "code". This
> could be a "thy_decl" command that updates the theory context by
> generated files that are accessible in Isabelle/ML, in addition to the
> export; it would also include a check for duplicate names.
> 
>   * "code_checking CONSTS in LANGUAGE" -- observing that "export_code
> ... checking" is actually a different command. It would be a "diag"
> command as before (this is relevant for parallelism).

Maybe the »checking« should just be a variant of the regular export.

Hence the modification could be quite conservative:

export_code CONSTS in LANGUAGE ( '(' OPTIONS ')' ) ( module_name NAME )
( file … | ( prefix … ) ( checked ) )

where »file« denotes a relative root in the file system and »checked«
indicated that the generated code will be checked implicitly.

So far my current thoughts.

Florian



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

[isabelle-dev] NEWS: generated code as proper theory export

[Florian Haftmann]

Code generation: command 'export_code' without file keyword exports
code as regular theory export, which can be materialized using tool
'isabelle export'; to get generated code dumped into output, use
'file ""'.  Minor INCOMPATIBILITY.

This refers to e02bdf853a4c and opens opportunities to get rid of ad-hoc
generated code in AFP-entries.

Florian



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

Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?

[Florian Haftmann]

>> Anyway, I am uncertain about the name »poll«.
> 
> From https://en.wikipedia.org/wiki/Cardinality
> 
> "Two sets A and B have the same cardinality if there exists a bijection from 
> A to B, that is, a function from A to B that is both injective and 
> surjective. Such sets are said to be equipotent, equipollent, or 
> equinumerous. This relationship can also be denoted A ≈ B or A ~ B.”

I see.  Using »poll« is a stem, the canonical names would be

less_eq_poll
equiv_poll
greater_eq_poll

(I don't know how useful the strict versions less_poll, greater_poll
would be).

Florian



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

Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?

[Florian Haftmann]

> I am inclined to introduce these definitions:
> 
> definition lepoll :: "'a set ⇒ 'b set ⇒ bool" (infixl "≲" 50)
> where "lepoll A B ≡ ∃f. inj_on f A ∧ f ` A ⊆ B"
> 
> definition eqpoll :: "'a set ⇒ 'b set ⇒ bool" (infixl "≈" 50)
> where "eqpoll A B ≡ ∃f. bij_betw f A B”
> 
> They allow, for example, this:
> 
> theorem Schroeder_Bernstein_eqpoll:
>   assumes "A ≲ B" "B ≲ A" shows "A ≈ B"
>   using assms unfolding eqpoll_def lepoll_def by (metis Schroeder_Bernstein)
> 
> The names and syntax are borrowed from Isabelle/ZF, and they are needed for 
> some HOL Light proofs.
> 
> But do they exist in some form already? And are there any comments on those 
> relation symbols?

The notation itself is quite generic, so it is worth spending more
thoughts on how can we keep reusable.  Maybe it would be worth a try to
put the syntax into a bundle (there are already some applications of
that pattern):

bundle set_relation_syntax
begin

notation …

end

bundle no_set_relation_syntax
begin

no_notation …

end

…

unbundle set_relation_syntax

…

unbundle no_set_relation_syntax

The input abbreviation gepoll should be added as well.

Anyway, I am uncertain about the name »poll«.

Cheers,
Florian



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

Re: [isabelle-dev] NEWS: support for GHC

[Florian Haftmann]

> * Support for Glasgow Haskell Compiler via command-line tools "isabelle
> ghc_setup", "isabelle ghci", "isabelle ghc", "isabelle ghc_stack".
> Existing settings variable ISABELLE_GHC is maintained dynamically
> according the state of ISABELLE_STACK_ROOT and ISABELLE_STACK_RESOLVER.

Just a side remark: I have tried »isabelle ghc_setup« and
»isabelle_ocaml_setup« and they work like a charm.

Florian



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

Re: [isabelle-dev] AFP/HLDE

[Florian Haftmann]

> Can 'export_code' do that, with a slight modification to produce formal
> exports via Export.export?

That what indeed be feasible.

Instead of "file", a keyword like "prefix" could be given to "export_code".

I will put this into my pipeline to implement, but it will take some
time until this will take shape, the code generator printing layers are
very technical.

Cheers,
Florian



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

Re: [isabelle-dev] AFP/HLDE

[Florian Haftmann]

Dear all,

> It seems to deliver an executable tool for later use elsewhere, but the
> implementation is very fragile.
> 
> We could take it as a model to get such a task right.

the situation wrt. generated code is indeed somehow baroque.

I am aware of the following layers / approaches:

a) Plain code generation to the file system (export_code … in … …); the
most basic use case.

b) Integration of code generation with the Isabelle/ML runtime; this
refers to evaluation and computations, and has reached a quite
satisfactory state.

c) Simple ad-hoc compilation checks (export_code … checking …) as
./src/HOL/Codegenerator_Test; this has always been mere device to check
that nothing utterly wrong has happended to the code generator.

d) Evaluation beyond Isabelle/ML (in src/HOL/Library/Code_Test.thy);
some kind of generalization of c).

What we have in $AFP/Diophantine_Eqns_Lin_Hom/Solver_Code.thy is
another, not-yet well integrated issue:

e) Using generated code in bigger integrative processes to derive build
results from it.  Also some kind of generalization of c).

There is indeed need for more »cultivation«, but IMHO we should resist
the temptation to put more and more programming language environment
interfaces into Isabelle: that would lead to mimic their divergent and
sophisticated concepts inside our environment (the reason why c) is
comparably simple to achieve is that out of 4 implemented target
languages Scala and SML are already well-integrated into Isabelle).

What about the other way round, i.e. integrating Isabelle into specific
programming language environments? It could work roughtly as follows:
* Generated code is a resource that can be exported from a session.
* Hence arbitrary programming language environment can use Isabelle to
obtain generated code.
* Its integration and compilation than happens just by existing tools of
that programming language environment, without burdening Isabelle at all.
* We would still need a way to integrate such constructs into our build
and session system, to express such things as »run this session, take
those results, put them into that programm call, expect the following
result and continue with …«; but this can maybe done by having a
construct in ROOT files which does not denote a regular theory session
but a operational logic implemented by a piece of Scala running in a
dedicated environment.

So far a few raw thoughts.

Cheers,
Florian




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

Re: [isabelle-dev] Frag / Poly_Mapping

[Florian Haftmann]

Just my five cent: instead of thinking about *integrating* the
developments, I'd suggest to distill their *common essence* into a
generic base theory, which would indeed be dedicated to functions with
finite support.

First-letter abbreviations are not very self-explanatory though.  So I'd
go with something more explicit like »finite_support_fun« – note that
this type constructor does not show up in concrete type syntax, only in
type class instantiations, so its length should be fine.

Cheers,
Florian

Am 24.09.2018 um 18:30 schrieb Manuel Eberl:
> Indeed, I am not sure whether avoiding duplication at all cost is what
> we should do here. poly_mapping is quite a big thing (and much essential
> material is still missing). It was introduced very specifically for the
> purpose of building monomials and polynomials. In principle, it can of
> course be seen in a much more general light. On the other hand, the free
> abelian groups have a more narrow focus.
> 
> Now, we could implement free abelian groups with poly_mapping. What
> would that entail? We would have to move it to the distribution, but
> then I think we should then also attempt to really clean it up quite a
> bit. Also, we would need to rename it to something catchy and more
> general. "Function with finite support" is what it essentially is, so
> perhaps "fsfun"?
> 
> Also, any changes that we make will have repercussions in the AFP and
> possibly other non-AFP applications (I'm concerned about IsaFoR in
> particular, so I cc'ed René).
> 
> Manuel
> 
> 
> On 24/09/2018 16:32, Lawrence Paulson wrote:
>>> On 24 Sep 2018, at 10:30, Alexander Maletzky 
>>>  wrote:
>>>
>>> Some notions defined in "Frag.thy" already exist in "Poly_Mapping.thy": 
>>> "support" is called "keys" there, and I think "frag_cmul" could easily be 
>>> defined in terms of "map".
>>>
>>> "frag_extend" looks like a special case of a more general subsitution 
>>> homomorphism "subst" of type "('a => 'b => 'c) => ('a =>_0 'b) => 'c", 
>>> defined as "subst f x = (\Sum i\in keys x. f i (lookup x i))", which could 
>>> indeed be added to "Poly_Mapping.thy". The insertion morphism in 
>>> "MPoly_Type.thy" could then perhaps be defined in terms of "subst" (at 
>>> least partially; for power-products, the above sum would have to be 
>>> replaced by a product).
>> Thanks for that. Manuel is expressing the opposite point of view, namely 
>> that it might be better to keep the two developments 100% separate. 
>> Certainly the basic setup of Frag is simple and short (see below) and we 
>> don't have to concern ourselves with how Poly_Mapping is used by other 
>> developments in the AFP and in other projects outside. So I'm puzzled as to 
>> the best course.
>>
>> Larry
>>
>> typedef 'a frag = "{f::'a\int. finite {x. f x \ 0}}"
>>   by (rule exI [where x = "\x. 0"]) auto
>>
>> definition support 
>>   where "support F = {a. Rep_frag F a \ 0}"
>>
>> declare Rep_frag_inverse [simp] Abs_frag_inverse [simp]
>>
>>
>> instantiation frag :: (type)comm_monoid_add
>> begin
>>
>> definition zero_frag_def: "0 \ Abs_frag (\x. 0)"
>>
>> definition add_frag_def: "a+b \ Abs_frag (\x. Rep_frag a x + 
>> Rep_frag b x)"
>>
>> lemma finite_add_nonzero: "finite {x. Rep_frag a x + Rep_frag b x \ 
>> 0}"
>> proof -
>>   have "finite {x. Rep_frag a x \ 0}" "finite {x. Rep_frag b x 
>> \ 0}"
>> using Rep_frag by auto
>>   moreover have "{x. Rep_frag a x + Rep_frag b x \ 0} \ {x. 
>> Rep_frag a x \ 0} \ {x. Rep_frag b x \ 0}"
>> by auto
>>   ultimately show ?thesis
>> using infinite_super by blast
>> qed
>>
>> lemma finite_minus_nonzero: "finite {x. - Rep_frag a x \ 0}"
>>   using Rep_frag [of a] by simp
>>
>> instance 
>> proof
>>   fix a b c :: "'a frag"
>>   show "a + b + c = a + (b + c)"
>> by (simp add: add_frag_def finite_add_nonzero add.assoc)
>> next
>>   fix a b :: "'a frag"
>>   show "a + b = b + a"
>> by (simp add: add_frag_def add.commute)
>> next
>>   fix a :: "'a frag"
>>   show "0 + a = a"
>> by (simp add: add_frag_def zero_frag_def)
>> qed
>>
>> end
>>
>> instantiation frag :: (type)ab_group_add
>> begin
>>
>> definition minus_frag_def: "-a \ Abs_frag (\x. - Rep_frag a 
>> x)"
>>
>> definition diff_frag_def: "a-b \ a + - (b::'a frag)"
>>
>> instance 
>> proof
>>   fix a :: "'a frag"
>>   show "- a + a = 0"
>> using finite_minus_nonzero [of a]
>> by (simp add: minus_frag_def add_frag_def zero_frag_def)
>> qed (simp add: diff_frag_def)
>>
>> end
>>
>>
>> definition frag_of where "frag_of c = Abs_frag (\a. if a = c then 1 
>> else 0)"
>>
>> lemma frag_of_nonzero [simp]: "frag_of a \ 0"
>> proof -
>>   have "(\x. if x = a then 1 else 0) \ (\x. 0::int)"
>> by (auto simp: fun_eq_iff)
>>   then have "Rep_frag (Abs_frag (\aa. if aa = a then 1 else 0)) 
>> \ Rep_frag (Abs_frag (\x. 0))"
>> by simp
>>   then show ?thesis
>> unfolding zero_frag_def frag_of_def Rep_frag_inject .
>> qed
>>
>> definition frag_cmul :: "int \ 'a frag \ 'a frag"
>>   where "frag_cmul 

Re: [isabelle-dev] Explorer.thy [was: performance problems]

[Florian Haftmann]

Hi all,

Am 12.09.2018 um 11:12 schrieb Lawrence Paulson:
> I regard it as indispensable. But it does need better pretty printing. 
> Also I greatly prefer the if/for format to assume/fix.

Am 12.09.2018 um 12:12 schrieb Mathias Fleury:
> I have my own version of explore
> (https://bitbucket.org/isafol/isafol/src/master/lib/Explorer.thy), which
> does not have better pretty printing, but has two variants that I find
> indispensable: explore_have produces "have … if … for …"
> and explore_lemma produces "lemma fixes … assumes … shows …". There is
> even an option for cartouches.

proper pretty printing should not be to difficult; maybe
Sledgehammer_Isar_Proof can be reused or a common base extracted from that.

explore_have should maybe just be the standard variant.

I would suggest a further variant

explore 

would actually be the same as

apply 

but, given a proof goal ‹!!ys. Qs ==> D›, for remaining goals ‹!!xs1.
Ps1 ==> C1› … ‹!!xsn. Psn ==> Cn› after method application suggest a
proof skeleton

proof -
  fix ys
  assume Qs
  have C1 if Ps1 for xs1
  moreover have C2 if Ps2 for xs2
  …
  moreover have Cn if Psn for xsn
  ultimately show D
by
qed 

and hence provide a way to quickly get to the essence of a proof after
initial »explore auto«.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Purpose of guess_infix

[Florian Haftmann]

Hi Makarius,

I guess this had something to do with Haskabelle, taking into account
its fundamental design flaw to write terms on its own rather than having
Isabelle's existing printing doing the job.

Since there is no reference left, it can be safely discarded.

Cheers,
Florian

Am 15.09.2018 um 21:32 schrieb Makarius:
> What is the purpose of guess_infix? It appears to be unused in current
> Isabelle/10da16970d82.
> 
> It orgininates from the following changeset:
> 
> changeset:   26678:a3ae088dc20f
> user:haftmann
> date:Wed Apr 16 10:50:37 2008 +0200
> files:   src/Pure/Syntax/parser.ML src/Pure/Syntax/syntax.ML
> description:
> educated guess for infix syntax
> 
> 
> The motivation behind the question: slightly more high-level access to
> notation, e.g. for export to other languages; possibly without "fishing"
> in the generated grammar.
> 
> 
>   Makarius
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Explorer.thy [was: performance problems]

[Florian Haftmann]

>> On 7 Sep 2018, at 19:18, Makarius  wrote:
>>
>> I can't try it out, since theory "Explorer" is missing.
> 
> Attached. A very cool thing. 

Nice to see that old draft from 5 years ago.

I would still agree that such a tool would be tremendously useful, but
before going into the distro it would need technical improvement, i.e.
more civilized approach toward Isar proof text generation, similar to
Sledgehammer_Isar_Proof.

Any opinions on that?

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Problems with newline in String.literal

[Florian Haftmann]

For the record: this issue has been resolved in
http://isabelle.in.tum.de/repos/isabelle/rev/25b431feb2e9.

Cheers,
Florian

Am 05.09.2018 um 10:32 schrieb Thiemann, René:
> Dear all,
> 
> I’m currently changing the error messages in our formalization from the 
> “string” type to
> “String.literal”, so that the exported code uses target language 
> strings in the generated code. Unfortunately, there seems to be a mistake
> in the handling of newline:
> 
> definition "message = STR ''this is⏎a two line text''"
> 
> is translated into Haskell as 
> 
> message :: String;
> message = "this is\\a two line text";
> 
> where the \\ should be a \n
> 
> Moreover, also the following behavior is weird:
> 
> lemma "STR ''⏎'' = STR 0x5C" "integer_of_char (CHR ''⏎'') = 10"
>   by code_simp+
> 
> Here, one observes that the ''⏎'' gets different characters codes, 
> depending on whether it is put into a CHR or into a STR.
> Note that 0x5C is precisely the backslash as in the generated Haskell code.
> 
> Cheers,
> René
> 
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] HOL/Computational_Algebra/Polynomial.thy

[Florian Haftmann]

> Is it right for this theory to base itself on HOL.Deriv rather than 
> Complex_Main?
> 
> Larry
> 
> section ‹Polynomials as type over a ring structure›
> 
> theory Polynomial
> imports
>   HOL.Deriv
>   "HOL-Library.More_List"
>   "HOL-Library.Infinite_Set"
>   Factorial_Ring
> begin

I don't think so, especially the combination of theories from
HOL-Library with a non-canonical theory entry is weird.

I am unable to tell on the spot how this has emerged.  Are there any
suspicious things when HOL.Deriv is replaces by Complex_Main?

I guess that theory uses some analytical results and hence cannot build
on Main alone.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

[Florian Haftmann]

>>> So we could provide "isabelle opam" as wrapper for something like "opam
>>> --root $ISABELLE_OPAM_HOME/$ISABELLE_PLATFORM64" as well as "isabelle
>>> opam_init" for the specific compiler version setup. Our component wiring
>>> would also provide ISABELLE_OCAML and ISABELLE_OCAMLC settings for the
>>> result.
>>
>> Do you intend to provide such a component for the 2018 release?
> 
> I was asking myself the same question yesterday: anything added at this
> stage needs to have some significance.

How significant is Isabelle as an integrative platform for OCaml?  The
code generator checks have been intended as a mere device to ensure that
nothing falls into disrepair (with all consequences regarding
infrastructure maintenance), but not as a development tool by itself.

So I would like to focus:
* What (upcoming) maintenance challenges are we facing?
* Are there particular applications out there which suggest more
integration with ocaml?
* …

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

[Florian Haftmann]

> No matter whether we decide to stick with Num or migrate to Zarith, the
> code generator needs to be updated to not link against "nums.cma" directly:
> 
>   val compile_cmd =
> "\"$ISABELLE_OCAMLC\" -w pu -o " ^ File.bash_path compiled_path ^
> " -I " ^ File.bash_path path ^
> " nums.cma " ^ File.bash_path code_path ^ " " ^ File.bash_path
> driver_path
> File.bash_path code_path ^ " " ^ File.bash_path driver_path
> 
> This is wrong, because it's not guaranteed where "nums.cma" is. The
> recommendation is to use "ocamlfind" instead. "ocamlfind" would be an
> extra dependency people would have to install, but a cursory search
> reveals that there are system packages for all major Linux
> distributions, macOS, and Cygwin.
> 
> Any thoughts on how to deal with this?

The best way maybe is to introduce a dedicated isabelle tool »ocamlc«
which uses an environment parameter ISABELLE_OCAML as path prefix to
ocamlc / ocamlfind; this would be more pleasant than any kind of ad-hoc
montage in ML.

Btw. Zarith is available at least since Ubuntu 16.04. as package
libzarith-ocaml.  It is anyway still unsatisfactory that such a
fundamental concept as proper integers does not work out-of-the-box

But there is now a possibility to have proper strings:
https://caml.inria.fr/pub/docs/manual-ocaml/libref/String.html

Maybe all these issues at a glance justify to modernized OCaml code
generation.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

[isabelle-dev] HOL-ODE-Numerics FAILED

[Florian Haftmann]

isabelle: 4acc029f69e9 tip
afp: c0882468fab2 tip

> HOL-ODE-Numerics FAILED
> (see also 
> /home/haftmann/.isabelle/heaps/polyml-5.7.1_x86_64-linux/log/HOL-ODE-Numerics)
>thm ->
>  int ->
>int ->
>  int ->
>int ->
>  (int * int * string) list ->
>string -> Proof.context -> int -> tactic
> val poincare'_bnds_tac = fn:
>thm ->
>  int ->
>int ->
>  int ->
>int ->
>  (int * int * string) list ->
>string -> Proof.context -> int -> tactic
> ### Rule already declared as elimination (elim)
> ### \(?f has_derivative ?f') ?F;
> ###  bounded_linear ?f' \ PROP ?W\
> ### \ PROP ?W
> ### theory "HOL-ODE-Numerics.Example_Utilities"
> ### 52.579s elapsed time, 113.340s cpu time, 12.052s GC time
> Loading theory "HOL-ODE-Numerics.ODE_Numerics"
> ### Introduced fixed type variable(s): 'b in "X__"
> ### theory "HOL-ODE-Numerics.ODE_Numerics"
> ### 0.056s elapsed time, 0.168s cpu time, 0.000s GC time
> *** Failed to apply initial proof method (line 985 of 
> "~/data/tum/afp/master/thys/Ordinary_Differential_Equations/Numerics/Runge_Kutta.thy"):
> *** using this:
> ***   convex (T \ X)
> ***   \x\T \ X.
> ***  ((\(t, x). f t x) has_derivative f' x)
> ***   (at x within T \ X)
> ***   \x\T \ X. onorm (f' x) \ B'
> ***   (t, x) \ T \ X
> ***   (t, y) \ T \ X
> *** goal (1 subgoal):
> ***  1. norm
> ***  ((case (t, x) of (t, x) \ f t x) -
> ***   (case (t, y) of (t, x) \ f t x))
> *** \ B' * norm ((t, x) - (t, y))
> *** At command "by" (line 985 of 
> "~/data/tum/afp/master/thys/Ordinary_Differential_Equations/Numerics/Runge_Kutta.thy")

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Cannot build HOL (again)

[Florian Haftmann]

Do the problems persist if you remove ~/.isabelle e.g. to ~/.isabelle_tmp?

Florian

Am 21.05.2018 um 16:23 schrieb Lawrence Paulson:
> Well, it worked on the third attempt. Same as two weeks ago. My guess is that 
> it pauses to wait for some resource: when it stalls, the process is still 
> visible but only uses 0.1% of the processor.
> 
> Larry
> 
>> On 21 May 2018, at 15:13, Manuel Eberl  wrote:
>>
>> It works fine for me.
>>
>> Did you perhaps switch on ML debugging/exception tracing? HOL becomes
>> virtually impossible to build with that switched on. What is the content
>> of your ".isabelle/etc/preferences”?
> 
> (* generated by Isabelle 25-Apr-2018 17:11:02 +0100 *)
> 
> auto_methods = "true"
> auto_nitpick = "true"
> auto_time_limit = "7.0"
> auto_time_start = ".5"
> auto_try0 = "false"  (* unknown *)
> editor_output_state = "true"
> editor_prune_delay = "60.0"
> editor_skip_proofs = "false"  (* unknown *)
> jedit_macos_application = "true"  (* unknown *)
> jedit_macos_preferences = "false"  (* unknown *)
> jedit_print_mode = "brackets"
> jedit_tooltip_delay = "0.5"
> parallel_proofs_threshold = "100"  (* unknown *)
> sledgehammer_provers = "e spass vampire z3 cvc4 "
> sledgehammer_timeout = "60"
> z3_non_commercial = "yes"  (* unknown *)
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] HOL-Algebra

[Florian Haftmann]

Hi all,

just a few comments on my behalf.

>> We’ve decided that Group-Ring-Module is irremediable, and are using it
>> only as a list of useful results that need to be done again.

Seems to make sense.

> Just one oddity in HOL-Algebra: It claims canonical theory names like> 
> "Group", "Ring", "Module". Thus the main HOL session needs to evade
via> non-standard names "Groups", "Rings", "Modules" (the latter is new
in> 2af1f142f855).

This pragmatic tradition had been started by »Orderings.thy«; I'm
uncertain whether it is worth the effort to change it.

Note that the theories »More_*.thy« contain material contributed by
Jeremy Avigad but not situated in HOL-Algebra in the first place; when
collecting this I did not want to touch the original theories, but as
part of a rework those theories could be integrated.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Slowdown of ConcurrentGC

[Florian Haftmann]

Hi Makarius,

> I have studied this a bit further. The interval
> 75130777ece4:d45b78cb86cf contains more than just the string type
> change, but it is still the main thing. Here are also other sessions in
> similar intervals 75130777ece4:0a6d6ba383dc, 75130777ece4:f76e8180c498:
> 
>   * faster: HOL-IMP, HOL-Quickcheck_Examples,
> Network_Security_Policy_Verification, Pre_Perron_Frobenius,
> JiveDataStoreModel, Partial_Function_MR
> 
>   * slower: Tarskis_Geometry, XML, Cauchy

distangling the ancient misunderstaning of char in Isabelle vs. various
character-related types in several target languages may indeed come at a
certain price in exotic situations; anyway I will have a look at those
sessions whether something meaningful can be derived from them.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Bad session structure: may cause problems with theory imports

[Florian Haftmann]

Hi Larry,

I guess you have to update your local AFP clone also.

Hope this helps,
Florian

Am 25.04.2018 um 18:03 schrieb Lawrence Paulson:
> In the past couple of days, upon launching Isabelle jEdit, I get an alert box 
> with the message above and the attached text. Any ideas?
> 
> Larry
> 
> ~/isabelle/Repos/src/Pure: hg id
> 362baebe25a5 tip
> 
> Cannot load theory "HOL-Library.Code_Char"
> The error(s) above occurred for theory "HOL-Library.Code_Char"
> (required by "Affine_Arithmetic.Affine_Arithmetic" via 
> "Affine_Arithmetic.Ex_Affine_Approximation" via "Affine_Arithmetic.Print") 
> (line 8 of "/Users/lp15/isabelle/afp/devel/thys/Affine_Arithmetic/Print.thy")
> No such file: "HOL-Library.Code_Char"
> The error(s) above occurred in session "HOL-ODE-Refinement" (line 19 of 
> "/Users/lp15/isabelle/afp/devel/thys/Ordinary_Differential_Equations/ROOT")
> Cannot load theory "HOL-Library.Code_Char"
> The error(s) above occurred for theory "HOL-Library.Code_Char"
> (required by "JinjaThreads.Basic_Main") (line 5 of 
> "/Users/lp15/isabelle/afp/devel/thys/JinjaThreads/Basic/Basic_Main.thy")
> No such file: "HOL-Library.Code_Char"
> The error(s) above occurred in session "JinjaThreads" (line 3 of 
> "/Users/lp15/isabelle/afp/devel/thys/JinjaThreads/ROOT")
> Cannot load theory "HOL-Library.Code_Char"
> The error(s) above occurred for theory "HOL-Library.Code_Char"
> (required by "DFS_Framework.DFS_Framework" via "DFS_Framework.Param_DFS" via 
> "CAVA_Base.CAVA_Base" via "CAVA_Base.CAVA_Code_Target" via 
> "CAVA_Base.Code_String") (line 9 of 
> "/Users/lp15/isabelle/afp/devel/thys/CAVA_Automata/CAVA_Base/Code_String.thy")
> No such file: "HOL-Library.Code_Char"
> The error(s) above occurred in session "Maxflow_Lib" (line 3 of 
> "/Users/lp15/isabelle/afp/devel/thys/Flow_Networks/ROOT")
> Cannot load theory "HOL-Library.Code_Char"
> The error(s) above occurred for theory "HOL-Library.Code_Char" (line 14 of 
> "/Users/lp15/isabelle/afp/devel/thys/Iptables_Semantics/ROOT")
> No such file: "HOL-Library.Code_Char"
> The error(s) above occurred in session "Iptables_Semantics" (line 3 of 
> "/Users/lp15/isabelle/afp/devel/thys/Iptables_Semantics/ROOT")
> Cannot load theory "HOL-Library.Code_Char"
> The error(s) above occurred for theory "HOL-Library.Code_Char"
> (required by "FOL_Harrison.FOL_Harrison") (line 14 of 
> "/Users/lp15/isabelle/afp/devel/thys/FOL_Harrison/FOL_Harrison.thy")
> No such file: "HOL-Library.Code_Char"
> The error(s) above occurred in session "FOL_Harrison" (line 3 of 
> "/Users/lp15/isabelle/afp/devel/thys/FOL_Harrison/ROOT")
> Cannot load theory "HOL-Library.Code_Char"
> The error(s) above occurred for theory "HOL-Library.Code_Char"
> (required by "LTL.LTL_Example") (line 9 of 
> "/Users/lp15/isabelle/afp/devel/thys/LTL/example/LTL_Example.thy")
> No such file: "HOL-Library.Code_Char"
> The error(s) above occurred in session "LTL" (line 3 of 
> "/Users/lp15/isabelle/afp/devel/thys/LTL/ROOT")
> Cannot load theory "HOL-Library.Code_Char"
> The error(s) above occurred for theory "HOL-Library.Code_Char"
> (required by "LLL_Factorization.Modern_Computer_Algebra_Problem") (line 13 of 
> "/Users/lp15/isabelle/afp/devel/thys/LLL_Factorization/Modern_Computer_Algebra_Problem.thy")
> No such file: "HOL-Library.Code_Char"
> The error(s) above occurred in session "LLL_Factorization" (line 3 of 
> "/Users/lp15/isabelle/afp/devel/thys/LLL_Factorization/ROOT")
> Cannot load theory "HOL-Library.Code_Char"
> The error(s) above occurred for theory "HOL-Library.Code_Char"
> (required by "Native_Word.Native_Cast") (line 8 of 
> "/Users/lp15/isabelle/afp/devel/thys/Native_Word/Native_Cast.thy")
> No such file: "HOL-Library.Code_Char"
> The error(s) above occurred in session "Native_Word" (line 3 of 
> "/Users/lp15/isabelle/afp/devel/thys/Native_Word/ROOT")
> Cannot load theory "HOL-Library.Code_Char"
> The error(s) above occurred for theory "HOL-Library.Code_Char"
> (required by "CAVA_Base.CAVA_Base" via "CAVA_Base.CAVA_Code_Target" via 
> "CAVA_Base.Code_String") (line 9 of 
> "/Users/lp15/isabelle/afp/devel/thys/CAVA_Automata/CAVA_Base/Code_String.thy")
> No such file: "HOL-Library.Code_Char"
> The error(s) above occurred in session "CAVA_Base" (line 3 of 
> "/Users/lp15/isabelle/afp/devel/thys/CAVA_Automata/ROOT")
> Cannot load theory "HOL-Library.Code_Char"
> The error(s) above occurred for theory "HOL-Library.Code_Char"
> (required by "Transition_Systems_and_Automata.NBA_Explicit" via 
> "Transition_Systems_and_Automata.NBA_Nodes" via 
> "DFS_Framework.Reachable_Nodes" via "DFS_Framework.DFS_Framework" via 
> "DFS_Framework.Param_DFS" via "CAVA_Base.CAVA_Base" via 
> "CAVA_Base.CAVA_Code_Target" via "CAVA_Base.Code_String") (line 9 of 
> "/Users/lp15/isabelle/afp/devel/thys/CAVA_Automata/CAVA_Base/Code_String.thy")
> No such file: "HOL-Library.Code_Char"
> The error(s) above occurred in session "Transition_Systems_and_Automata" 
> (line 3 of 
> 

Re: [isabelle-dev] NEWS: Latex errors

[Florian Haftmann]

> *** Document preparation ***
> 
> * Command-line tool "isabelle document" has been re-implemented in
> Isabelle/Scala, with simplified arguments and explicit errors from the
> latex process. Minor INCOMPATIBILITY.

That explicit error reporting is a great thing missed for so long!

Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

[isabelle-dev] Haskabelle unmaintained

[Florian Haftmann]

Hi all,

I see that the old Haskabelle website is still a regular part of the
Isabelle website: http://isabelle.in.tum.de/haskabelle.html

Since Haskabelle is no out of maintainance it is outdated and should be
removed.  What is the recommended procedure for this?

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Slow builds due to excessive heap images

[Florian Haftmann]

> They are just identifiers and I don't think they are computed with.
> However, I don't intend to change formalization beyond a global
> implementation of int by some fixed size integers, if that can be done
> easily. Otherwise we live with the increase in runtime from 7:20 to 8:20.

Hence a suitable theory would follow Code_Numeral and provide
code_printing declarations to map integer to a fixed-width
overflow-guarding implementation.

But I am also not sure whether this is worth the effort.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Slow builds due to excessive heap images

[Florian Haftmann]

Dear all,

> The idea above is to provide an option for the HOL codegen that is used
> specifically for applications like Flyspeck-Tame. It is mainly a
> question to codegen experts, if that can be done easily.

streamlining execution of Flyspeck-Tame without risking its integrity is
a struggle now carrying on twelve years.

The key question to me is whether the integers in the archives (the ML
files) are actually used for numeric calculation (+, *, …) or are just
mere identifiers (=, maybe <).  In the latter case there are a couple of
possibilities not explored so far.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] NEWS: more options for "isabelle jedit"

[Florian Haftmann]

Dear Makarius,

> *** Prover IDE -- Isabelle/Scala/jEdit ***
> 
> * The command-line tool "isabelle jedit" provides more flexible options
> for session selection:
>   - options -P opens the parent session image of -l
>   - options -A and -B modify the meaning of -l to produce a base
> image on the spot, based on the specified ancestor (or parent)
>   - option -F focuses on the specified logic session
>   - option -R has changed: it only opens the session ROOT entry
>   - option -S sets up the development environment to edit the
> specified session: it abbreviates -B -F -R -l
> 
>   Examples:
> isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
> isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis

this is really great and makes my life significantly easier!

There remains one gap which I am wondering how to fill it.

Lets start with

isabelle jedit -d '$AFP' -S …

This provides a suitable base image and opens the ROOT file.

What is the canonical way to proceed from there to check the whole
session?  Of course the ROOT file lists the respective theories and you
can open them manually in jedit, but this is tiresome if the ROOT file
spans many theories.

Would clicakble theorie files in ROOT files be an option?

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Future of Nat_Transfer

[Florian Haftmann]

See now http://isabelle.in.tum.de/repos/isabelle/rev/0230af0f3c59.

Florian

Am 19.10.2017 um 13:56 schrieb Florian Haftmann:
> Dear all,
> 
> the nowadays ancient theory Nat_Transfer (essentially providing an
> attribute to transfer ad-hoc between theorems on nat vs. int) is almost
> obsolete:
> 
> * »almost« since I haven't figured out how relevant it is still for
> HOL-Number_Theory
> 
> * Conversion between nat and int is rarely needed since most common
> lemmas are provided by type classes anyway nowadays.
> 
> See also
> http://isabelle.in.tum.de/repos/isabelle/file/ee874941dfb8/src/HOL/Nat_Transfer.thy
> for the current state of affairs.
> 
> My suggestion would be to remove it completely.
> 
> Any opinions on that?
> 
> Cheers,
>   Florian
> 
> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] linordered_semiring_1

[Florian Haftmann]

See now http://isabelle.in.tum.de/repos/isabelle/rev/a1a4a5e2933a

Cheers
Florian

Am 28.10.2017 um 16:14 schrieb Florian Haftmann:
> Hi Akihisa,
> 
> thanks for pointing that out.
> 
> I will take care of this.
> 
> All the best,
>   Florian
> 
> Am 20.10.2017 um 17:37 schrieb Yamada, Akihisa:
>> Dear Isabelle/HOL developers,
>>
>> I propose to make linordered_semiring_1 a subclass of zero_less_one.
>>
>> class linordered_semiring_1 =
>>linordered_semiring + semiring_1 + zero_less_one
>>
>> (Of course, zero_less_one should be defined earlier.)
>>
>> Currently, it does not assume 0 < 1, but this generality allows only 
>> nonsense (and confusing) instances as the assumptions of 
>> ordered_semiring is applicable only if there is some positive element, 
>> which cannot exist if 0 < 1.
>>
>> lemma (in linordered_semiring_1)
>>assumes a0: "0 < a" shows "0 < 1"
>> proof (rule ccontr)
>>assume "¬ 0 < 1" then have "1 ≤ 0" by auto
>>from mult_nonpos_nonneg[OF this] a0 have "a ≤ 0" by auto
>>with a0 show False by auto
>> qed
>>
>> Best regards,
>> Akihisa
>> ___
>> isabelle-dev mailing list
>> isabelle-...@in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
> 
> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] linordered_semiring_1

[Florian Haftmann]

Hi Akihisa,

thanks for pointing that out.

I will take care of this.

All the best,
Florian

Am 20.10.2017 um 17:37 schrieb Yamada, Akihisa:
> Dear Isabelle/HOL developers,
> 
> I propose to make linordered_semiring_1 a subclass of zero_less_one.
> 
> class linordered_semiring_1 =
>linordered_semiring + semiring_1 + zero_less_one
> 
> (Of course, zero_less_one should be defined earlier.)
> 
> Currently, it does not assume 0 < 1, but this generality allows only 
> nonsense (and confusing) instances as the assumptions of 
> ordered_semiring is applicable only if there is some positive element, 
> which cannot exist if 0 < 1.
> 
> lemma (in linordered_semiring_1)
>assumes a0: "0 < a" shows "0 < 1"
> proof (rule ccontr)
>assume "¬ 0 < 1" then have "1 ≤ 0" by auto
>from mult_nonpos_nonneg[OF this] a0 have "a ≤ 0" by auto
>with a0 show False by auto
> qed
> 
> Best regards,
> Akihisa
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Unexpected auto indent in 13a1081961d2

[Florian Haftmann]

>> the attached theory is the (unexpected) result of typing its content
>> naively and relying on auto indent.
>>
>> Do others experience the same or is it maybe a settings problem?
> 
> Can you check $ISABELLE_HOME_USER/etc/preferences if there are any
> changes on jedit_indent_input, jedit_indent_newline,
> jedit_indent_script, jedit_indent_script_limit?
> 
> There is also a section about "Indentation" in the Isabelle/jEdit plugin
> options dialog.
> 
> Basically everything should be set to the defaults for the best
> experience, although there are sometimes old habits to overcome as usual.
> 
> You can also try http://isabelle.in.tum.de/website-Isabelle2017-RC1 with
> its fresh environment.

Deleting $ISABELLE_HOME_USER/etc/jedit worked, thanks.

Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

[isabelle-dev] Unexpected auto indent in 13a1081961d2

[Florian Haftmann]

Dear all,

the attached theory is the (unexpected) result of typing its content
naively and relying on auto indent.

Do others experience the same or is it maybe a settings problem?

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
theory Foo
imports Main
begin

definition I :: "'a \ 'a"
where "I x = x"

definition K :: "'b \ 'a \ 'a"
where "K x = I"

lemma K_apply:
  "K y x = x"
  by (simp add: K_def I_def)

lemma nonsense:
  "2 * n div 2 = n" if "even n" for n :: nat
  proof (cases "even n")
  case True
  then show ?thesis
  by simp
  next
  case False
  with that show ?thesis
  by simp
  qed
  

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

Re: [isabelle-dev] Towards the Isabelle2017 release

[Florian Haftmann]

Hi Rene,

> =
> locale foo = fixes f :: "nat => nat"
>   assumes f_mono[termination_simp]: "f x <= x"
> begin
> 
> fun bar :: "nat => nat" where
>   "bar 0 = 0"
> | "bar (Suc x) = Suc (bar (f x))"
> 
> end
> 
> definition com where
>   [code del]: "com = foo.bar id"
> 
> interpretation foo id
>   rewrites "foo.bar id = com"
>   unfolding com_def by (unfold_locales, auto)
> 
> lemma "com 5 = 5" by eval
> export_code com in Haskell
> =
> 
> 
> This works perfectly fine in Isabelle 2016-1, and especially
> the [code del] is required to make the final export_code and eval succeed.
> 
> In contrast, in a recent development version, the [code del] still is 
> accepted,
> but the export_code will deliver “com _ = error …” and the “eval” will fail.
> 
> The solution is easy: remove the previously required [code del].

this is due to subtle changes in the semantics of [code del] which now
merely removes a single equation from a list of concrete function
equations; strict removal of a function declaration is now done using
[[code drop: …]].

Note that the pattern above is avoided nowadays by an interpretation
with mixin definitions:

theory Bar
  imports Main
begin

locale foo = fixes f :: "nat => nat"
  assumes f_mono [termination_simp]: "f x ≤ x"
begin

fun bar :: "nat => nat" where
  "bar 0 = 0"
| "bar (Suc x) = Suc (bar (f x))"

end

global_interpretation foo id
  defines com = bar
  by standard simp

lemma "com 5 = 5" by eval
export_code com in Haskell

end

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] \mu and \nu in HOL-Algebra [was Re: Towards the Isabelle2017 release]

[Florian Haftmann]

Hi Clemens,

>>   If one imports HOL-Algebra.Multiplicative_Group (which we actually do
>>   via some transitive import), then \mu (LFP), \nu (GFP) and
>>   \phi (Euler’s totient function) become constants.
> 
> Unless I hear otherwise I will replace \mu by LFP and \nu by GFP.

sorry, I didn't recognize your follow-up message to this thread until now.

Of course you are free to go ahead and revert the workaround e.g. using
hg backout 5a42eddc11c1

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] HOL-Computational_Algebra and Polynomial_Factorial

[Florian Haftmann]

> Is it intentional that the "Computational_Algebra" theory does not
> import "Polynomial_Factorial"?

Yes.  Polynomial_Factorial requires Field_as_Ring, which does a
substantial modification to the type class hierarchy, pulling it apart
from long-established traditions in HOL-Main.  I have been reluctant to
enforce this on any material derived from the session entry point.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Towards the Isabelle2017 release

[Florian Haftmann]

Am 24.08.2017 um 22:39 schrieb Manuel Eberl:
> On 2017-08-24 17:34, Florian Haftmann wrote:
>> I would still appreciate if someone would take the comment »Deviates
>> from the definition given in the library in number theory« as a starting
>> point to reconcile that definition with src/HOL/Number_Theory/Totient.thy.
> 
> Oh actually I fixed that a few months ago. I even wrote on the mailing
> list back then, I think. Those definitions should now be equivalent.

This sound good.

> I didn't know there was a totient function in HOL-Algebra, otherwise I
> would have removed the duplicate back then.

I had a look at it; I think to reconcile it we would have to move
Totient.thy to Library/, otherwise there would be a dependency cycle.

Looks like something to be done not before the next release.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Towards the Isabelle2017 release

[Florian Haftmann]

For the final record:

> \phi is the result of a simple typo accident
see http://isabelle.in.tum.de/repos/isabelle/rev/ba94aeb02fbc

> Concerning \mu and \nu, I am currently investigating whether an import
> swap could re-establish the situation known from Isabelle2016-1

see http://isabelle.in.tum.de/repos/isabelle/rev/5a42eddc11c1

Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Towards the Isabelle2017 release

[Florian Haftmann]

Hi Rene,

> - In the NEWS I read about freeing short constant names like the
>   “Renamed ii to imaginary_unit in order to free up ii as a variable”.
>   I definitely support this kind of change, but at the same time found
>   quite the opposite in HOL-Algebra:
>   If one imports HOL-Algebra.Multiplicative_Group (which we actually do
>   via some transitive import), then \mu (LFP), \nu (GFP) and 
>   \phi (Euler’s totient function) become constants.
>   This was a bit annoying.

thanks for pointing that out.

\phi is the result of a simple typo accident (cf.
http://isabelle.in.tum.de/repos/testboard/rev/6c818fc0c817).

I would still appreciate if someone would take the comment »Deviates
from the definition given in the library in number theory« as a starting
point to reconcile that definition with src/HOL/Number_Theory/Totient.thy.

Concerning \mu and \nu, I am currently investigating whether an import
swap could re-establish the situation known from Isabelle2016-1
(http://isabelle.in.tum.de/repos/testboard/rev/0ad153ee9ece).

> - There have been some changes w.r.t. code-generation which now lead
>   to runtime exception in the generated code. For instance, now
>   I get code like
>   “f x = Code.abort …” 
>   whereas in 2016-1 there was a proper code like
>   “f x = some ordinary right-hand side” 
>   We did not yet isolate the problem and will report later.

OK, I will dig into this after you have isolated it.  Might be well that
this only occurs on certain theory merges.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

[isabelle-dev] Problem in AFP

[Florian Haftmann]

isabelle: 9a4c049f8997 tip
afp: af801987e595 tip
Running Separation_Logic_Imperative_HOL ...
*** Undefined fact: "sum_list_update_nat" (line 598 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Separation_Logic_Imperative_HOL/Examples/Hash_Table.thy")
*** At command "from" (line 598 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Separation_Logic_Imperative_HOL/Examples/Hash_Table.thy")
*** Undefined fact: "sum_list_update_nat" (line 580 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Separation_Logic_Imperative_HOL/Examples/Hash_Table.thy")
*** At command "from" (line 580 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Separation_Logic_Imperative_HOL/Examples/Hash_Table.thy")
*** Undefined fact: "sum_list_update_nat" (line 374 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Separation_Logic_Imperative_HOL/Examples/Hash_Table.thy")
*** At command "from" (line 374 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Separation_Logic_Imperative_HOL/Examples/Hash_Table.thy")
*** Undefined fact: "sum_list_update_nat" (line 356 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Separation_Logic_Imperative_HOL/Examples/Hash_Table.thy")
*** At command "from" (line 356 of
"/mnt/home/haftmann/data/tum/afp/master/thys/Separation_Logic_Imperative_HOL/Examples/Hash_Table.thy")
Unfinished session(s): Separation_Logic_Imperative_HOL
0:02:11 elapsed time, 0:07:54 cpu time, factor 3.62

Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] [isabelle] Good name for "sublist" predicates

[Florian Haftmann]

Just for the record:

* Topological_Spaces.subseq has already been present before 2007 in
HOL/Hyperreal/SEQ.thy (cf. eb85850d3eb7)

* strict_mono has entered in 2009, see abefe1dfadbb

Hence we have the typical situation that a generalized constant subsumes
a more ancient unconsciously.

Cheers,
Florian

Am 30.06.2017 um 20:41 schrieb Manuel Eberl:
> On 2017-06-30 20:33, Sebastien Gouezel wrote:
>> I used subseq quite heavily in my ergodic theory developments. From
>> a mathematician point of view, taking subsequences of sequences
>> from nat to nat is very common and very useful in analysis (much
>> more than taking subsequences of lists).
> 
> So what about the suggestion of just writing "strict_mono" instead?
> Besides, you can always introduce local abbreviations for things with
> "notation" and delete them with "no_notation" afterwards.
> 
>> By the way, I recently encountered a similar (and even more nasty)
>> name clash, with compact. The following works perfectly
> 
> It's "Topological_Spaces.compact" and that should definitely work. We
> should probably make the one from Complete_Partial_Order2 qualified. In
> my opinion, there is no question that "compact" should be "compact" in
> the topological sense.
> 
> Cheers,
> 
> Manuel
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] scala-2.12.2

[Florian Haftmann]

See now finally http://isabelle.in.tum.de/repos/isabelle/rev/a41435469559

Florian

Am 23.06.2017 um 08:43 schrieb Lars Hupel:
>> The patch is now running on testboard:
>> .
> 
> Unfortunately, this patch did not work out.
> 
> 22:13:39 *** Failed to finish proof (line 62 of
> "~~/src/HOL/Library/Code_Target_Nat.thy"):
> 22:13:39 *** goal (1 subgoal):
> 22:13:39 ***  1. Transfer.Rel (rel_fun pcr_integer (rel_fun op = op =))
> 22:13:39 ***  (\a b. True) op =
> 22:13:39 *** At command "by" (line 62 of
> "~~/src/HOL/Library/Code_Target_Nat.thy")
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] scala-2.12.2

[Florian Haftmann]

> Alternatively, Florian might offer some insight why he set up the code
> equations for that particular constant in that way (see "String.thy",
> where a ML snippet generates 256 code equations). Note that large
> pattern matches on the JVM should be avoided, lest we violate the 64k
> method length limit in class files ("integer_of_char" currently requires
> 58044 bytes).

I took the opportunity to have a look at it and found out it can be done
differently, see attached patch.

The clue about "integer_of_char" is that it had to work regardless
whether HOL chars are represented authentic or by target language
characters (importing "~~/src/HOL/Library/Code_Char").

Nowadays this can be achieved without spelling out the chars explicitly.
 The last stone to turn around before had been the de-constructivation
of the char type (b3f2b8c906a6).

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
# HG changeset patch
# Parent  45d3d43abee7147fd43e63a6b4ba6340a5d4b74f
more direct construction of integer_of_num;
code equations for integer_of_char may rely on pattern matching on Char

diff -r 45d3d43abee7 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy  Thu Jun 22 16:59:14 2017 +0200
+++ b/src/HOL/Code_Numeral.thy  Thu Jun 22 17:31:28 2017 +0200
@@ -149,24 +149,19 @@
   "int_of_integer (Num.sub k l) = Num.sub k l"
   by transfer rule
 
-lift_definition integer_of_num :: "num \ integer"
-  is "numeral :: num \ int"
-  .
+definition integer_of_num :: "num \ integer"
+  where [simp]: "integer_of_num = numeral"
 
 lemma integer_of_num [code]:
-  "integer_of_num num.One = 1"
-  "integer_of_num (num.Bit0 n) = (let k = integer_of_num n in k + k)"
-  "integer_of_num (num.Bit1 n) = (let k = integer_of_num n in k + k + 1)"
-  by (transfer, simp only: numeral.simps Let_def)+
-
-lemma numeral_unfold_integer_of_num:
-  "numeral = integer_of_num"
-  by (simp add: integer_of_num_def map_fun_def fun_eq_iff)
+  "integer_of_num Num.One = 1"
+  "integer_of_num (Num.Bit0 n) = (let k = integer_of_num n in k + k)"
+  "integer_of_num (Num.Bit1 n) = (let k = integer_of_num n in k + k + 1)"
+  by (simp_all only: integer_of_num_def numeral.simps Let_def)
 
 lemma integer_of_num_triv:
   "integer_of_num Num.One = 1"
   "integer_of_num (Num.Bit0 Num.One) = 2"
-  by (transfer, simp)+
+  by simp_all
 
 instantiation integer :: "{linordered_idom, equal}"
 begin
@@ -301,7 +296,7 @@
 end
 
 declare divmod_algorithm_code [where ?'a = integer,
-  unfolded numeral_unfold_integer_of_num, unfolded integer_of_num_triv, 
+  folded integer_of_num_def, unfolded integer_of_num_triv, 
   code]
 
 lemma integer_of_nat_0: "integer_of_nat 0 = 0"
diff -r 45d3d43abee7 src/HOL/String.thy
--- a/src/HOL/String.thyThu Jun 22 16:59:14 2017 +0200
+++ b/src/HOL/String.thyThu Jun 22 17:31:28 2017 +0200
@@ -160,35 +160,10 @@
   by (simp only: integer_of_char_def integer_of_nat_def comp_apply 
nat_of_char_Char map_fun_def
 id_apply zmod_int modulo_integer.abs_eq [symmetric]) simp
 
-lemma less_256_integer_of_char_Char:
-  assumes "numeral k < (256 :: integer)"
-  shows "integer_of_char (Char k) = numeral k"
-proof -
-  have "numeral k mod 256 = (numeral k :: integer)"
-by (rule semiring_numeral_div_class.mod_less) (insert assms, simp_all)
-  then show ?thesis using integer_of_char_Char [of k]
-by (simp only:)
-qed
-
-setup \
-let
-  val chars = map_range (Thm.cterm_of @{context} o HOLogic.mk_numeral o curry 
(op +) 1) 255;
-  val simpset =
-put_simpset HOL_ss @{context}
-  addsimps @{thms numeral_less_iff less_num_simps};
-  fun mk_code_eqn ct =
-Thm.instantiate' [] [SOME ct] @{thm less_256_integer_of_char_Char}
-|> full_simplify simpset;
-  val code_eqns = map mk_code_eqn chars;
-in
-  Global_Theory.note_thmss ""
-[((@{binding integer_of_char_simps}, []), [(code_eqns, [])])]
-  #> snd
-end
-\
-
-declare integer_of_char_simps [code]
-
+lemma integer_of_char_Char_code [code]:
+  "integer_of_char (Char k) = integer_of_num k mod 256"
+  by simp
+  
 lemma nat_of_char_code [code]:
   "nat_of_char = nat_of_integer \ integer_of_char"
   by (simp add: integer_of_char_def fun_eq_iff)


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

[isabelle-dev] Issue in AFP

[Florian Haftmann]

> isabelle: 20304512a33b tip
> afp: 644957b424ee tip
> JinjaThreads FAILED
> (see also 
> /srv/data/tum/isabelle/master/heaps/polyml-5.6_x86-linux/log/JinjaThreads)
> ***(\T.
> ***typeof\<^bsub>h\<^esub> v =
> ***\T\ \
> ***(\C.
> ***class_type_of' T =
> ***\C\ \
> ***(\Ts Tr D.
> ***  P \ C sees M: Ts\Tr = Native in D 
> \
> ***  \external_defs D M
> ***then (\red0t (extTA2J0 P) P t h
> ***   (Val v\M(es), xs)
> ***   (Val v\M(es'), xs') \
> ***  countInitBlock (Val v\M(es1'))
> ***  < countInitBlock (Val v\M(es1)) 
> \
> ***  Val v\M(es') =
> ***  Val v\M(es) \
> ***  xs' = xs) \
> *** h' = h \
> *** ta1 = \\ \
> *** ta = \\
> ***else ta_bisim01 ta (extTA2J1 (compP1 P) ta1) \
> *** (if call (Val v\M(es)) = None \
> *** call1 (Val v\M(es1)) = None
> ***  then \e'' xs''.
> ***  \red0r (extTA2J0 P) P t h
> *** (Val v\M(es), xs) (e'', xs'') \
> ***  extTA2J0
> *** P,P,t \ \e'',(h, xs'')\ -ta\
> ***\Val v\M(es'),(h', xs')\ \
> ***  no_call P h e'' \
> ***  \ \move0 P h e''
> ***  else extTA2J0
> ***P,P,t \ \Val
> ***   v\M(es),
> ***  (h, xs)\ -ta\
> *** \Val v\M(es'),(h', xs')\ \
> ***   no_call P h (Val v\M(es)) \
> ***   \ \move0 P h
> *** (Val v\M(es
> *** At command "apply" (line 911 of 
> "/srv/data/tum/afp/master/thys/JinjaThreads/Compiler/Correctness1.thy")

Any hint what is going on?

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] scala-2.12.2

[Florian Haftmann]

Am 11.06.2017 um 09:01 schrieb Florian Haftmann:
>> It definitely looks like scala-2.12.2 causes non-termination, e.g. of
>> src/HOL/Codegenerator_Test/Generate.thy -- I have opened that file in
>> isabelle jedit and waited for approx. 30min; a batch build of
>> HOL-Codegenerator_Test ran into timeout of 2h.
>>
>> Maybe Florian has an idea.

Unfortunately I cannot reproduce this.

Starting with a2e441805d6a, I did a

hg backout 94b0da1b242e

and neither src/HOL/Codegenerator_Test/Generate.thy nor
src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy exposed
any problems.

I took the generated code and ran separate Scala compilations:

> + /home/haftmann/.isabelle/contrib/scala-2.11.8/bin/scalac -encoding UTF-8 
> -nowarn -target:jvm-1.8 -Xmax-classfile-name 130 -J-Xms128m -J-Xmx1024m 
> -J-Xss2m scala_12.scala
> 
> real  0m59.888s
> user  2m2.836s
> sys   0m0.848s
> 
> + /home/haftmann/.isabelle/contrib/scala-2.12.2/bin/scalac -encoding UTF-8 
> -nowarn -target:jvm-1.8 -Xmax-classfile-name 130 -J-Xms128m -J-Xmx1024m 
> -J-Xss2m scala_12.scala
> 
> real  1m55.739s
> user  3m8.200s
> sys   0m0.760s

Surely there is a considerable increase in time resources but no
termination issue at all.

Maybe we should give it another try?

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] scala-2.12.2

[Florian Haftmann]

> It definitely looks like scala-2.12.2 causes non-termination, e.g. of
> src/HOL/Codegenerator_Test/Generate.thy -- I have opened that file in
> isabelle jedit and waited for approx. 30min; a batch build of
> HOL-Codegenerator_Test ran into timeout of 2h.
> 
> Maybe Florian has an idea.

Btw. I am working on this but still have no conclusive answer.

To be continued…

Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

[isabelle-dev] Build Problem in JinjaThreads

[Florian Haftmann]

isabelle: 3bec939bd808 tip
afp: 09eedef13195 tip

> ***   {n. enat n < llength stls \
> ***   (case lnth stls n of
> ***(s, tl, s') \ \ \move s tl s')} ::
> ***   nat set
> *** 
> *** Coercion Inference:
> *** 
> *** Local coercion insertion on the operand failed:
> *** Cannot generate coercion from "??'a26 set" to "'a"
> *** 
> *** Now trying to infer coercions globally.
> *** 
> *** Coercion inference failed:
> *** weak unification of subtype constraints fails
> *** 
> *** 
> *** At command "hence" (line 512 of 
> "/mnt/home/haftmann/data/tum/afp/master/thys/JinjaThreads/Framework/LTS.thy")
> *** Type unification failed
> *** 
> *** Type error in application: incompatible operand type
> *** 
> *** Operator:  lsublist tls :: 'a \ 'tl llist
> *** Operand:
> ***   {n. enat n < llength stls \
> ***   (case lnth stls n of
> ***(s, tl, s') \ \ \move s tl s')} ::
> ***   nat set
> *** 
> *** Coercion Inference:
> *** 
> *** Local coercion insertion on the operand failed:
> *** Cannot generate coercion from "??'a26 set" to "'a"
> *** 
> *** Now trying to infer coercions globally.
> *** 
> *** Coercion inference failed:
> *** weak unification of subtype constraints fails
> *** 
> *** 
> *** At command "hence" (line 512 of 
> "/mnt/home/haftmann/data/tum/afp/master/thys/JinjaThreads/Framework/LTS.thy")

Any suggestion what is going on here?

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] NEWS: GCD and Binomial in Main

[Florian Haftmann]

>> Are there good ideas how to do it with Binomial? Thus we could get rid
>> of the Pre_Main theory from f533820e7248.
> 
> The import could be changed e.g. to Groups_List.
> 
> Desirable would also be to split the theory into Factorial and Binomial,
> to raise awareness of existing combinatorial material in HOL.

See now bdd17b18e103.

Theory Pre_Main is still present, but now trivial to get rid of.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] NEWS: GCD and Binomial in Main

[Florian Haftmann]

Am 25.04.2017 um 11:06 schrieb Manuel Eberl:
> I think you actually solved that problem by now. If I recall correctly,
> it was one of the two dictionary-related problems I told you about a
> year ago or so, and then Lars and you solved that problem somehow.
> 
> I can try putting in that code equation again and seeing what happens.

Excellent, thanks.

Florian

> 
> 
>>> (*TODO: This code equation breaks Scala code generation in 
>>> HOL-Codegenerator_Test. We have to figure out why and how to prevent that. 
>>> *)
> 
> Manuel
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] NEWS: GCD and Binomial in Main

[Florian Haftmann]

> * Theories "GCD" and "Binomial" are already included in "Main" (instead
> of "Complex_Main").
> 
> 
> This refers to Isabelle/f533820e7248: the change came up while exploring
> theory imports systematically. Normally, only "Main" or "Complex_Main"
> should be imported from the HOL session, not anything in between. (This
> is a concession to the complex bootstrap process of HOL.)
> 
> In Isabelle/85ed070017b7 Florian has already improved the imports of GCD
> further.
> 
> Are there good ideas how to do it with Binomial? Thus we could get rid
> of the Pre_Main theory from f533820e7248.

The import could be changed e.g. to Groups_List.

Desirable would also be to split the theory into Factorial and Binomial,
to raise awareness of existing combinatorial material in HOL.

As an aside, maybe someone is eager to take the comment

> (*TODO: This code equation breaks Scala code generation in 
> HOL-Codegenerator_Test. We have to figure out why and how to prevent that. *)

seriously.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Code generation: privacy of exported types in signatures

[Florian Haftmann]

Dear Frédéric,

> Your previous example works because it is foo which is given to deps_of
> as argument, not the constant C. So one way for calling deps_of with C
> is to replace foo by C:
> export_code C in SML
> (or also by writing @{code C} in ML)

ok, now I can follow your observations.

> [...] In my previous answer, apart from modifying deps_of
> there are actually several ways of fixing that, then of course any
> over-approximations on export_code look good to me, as long as it does
> not differ too much from code_reflect... (or @{code}, for instance I
> hope its semantical change was intentional during the introduction of
> @{computation})

It has not been an intentional semantical change, but a clarification of
the implementation as side benefit of the whole @{computation} story.

You might try in the next Isabelle release (not scheduled yet) whether
your issues still persist, or maybe check against a recent ongoing
development revision.

Hope this helps,
Florian

> 
> Best,
> Frédéric
> 
> 
> Fri, 14 Apr 2017 10:09:38 +0200, Florian Haftmann : 
> 
> 
>> Dear Frédéric,
>>
>> I cannot follow reproduce observation; using the attached theory in
>> Isabelle2016-1, I get
>>
>>> structure Foo : sig
>>>   type 'a b
>>>   type 'a c
>>>   val foo : 'a b -> 'a b
>>> end = struct
>>>
>>> datatype 'a a = A;
>>>
>>> datatype 'a b = B of 'a c a
>>> and 'a c = C of 'a b;
>>>
>>> fun foo x = x;
>>>
>>> end; (*struct Foo*)
>> which is almost perfectly fine, apart from the superfluous 'a c export.
>>
>> How does your theory and export_code statement exactly look like?
>>
>> Two points to note anyway:
>>
>> * This question would belong to the user (published release) rather than
>> the development (ongoing changes to a central code repository) mailing list.
>>
>> * The implementation of code exports is an over-approximation.  This is
>> a known issue but not very likely to be addressed in the near future.
>>
>> Cheers,
>>  Florian
>>
>>
>> Am 09.04.2017 um 08:04 schrieb Frederic Tuong (Dr):
>>> Dear all,
>>>
>>> The SML generated code of the following snippet is not well typed
>>> anymore since Isabelle 2014:
>>>
>>> datatype 'a A = aaa
>>> datatype 'a B = bbb "'a C A"
>>>  and 'a C = ccc "'a B"
>>>
>>> This is because when computing types to be marked as not private (during
>>> the generation of the signature of A, B and C), A has not been assigned
>>> as an "Opaque" type, where the constructor Opaque is defined in
>>> ~~/src/Tools/Code/code_namespace.ML .
>>>
>>> One solution is to replace the function deps_of defined in line 94 of
>>> http://isabelle.in.tum.de/repos/isabelle/file/7dd1971b39c1/src/Tools/Code/code_namespace.ML
>>> by this function:
>>>
>>> fun deps_of sym =
>>>   let
>>> val succs1 = Code_Symbol.Graph.Keys.dest o
>>> Code_Symbol.Graph.imm_succs gr;
>>> fun succs2 x = Code_Symbol.Graph.all_succs gr [x];
>>> val deps1 = succs1 sym;
>>> val deps2 = [] |> fold (union (op =)) (map succs2 deps1) |>
>>> subtract (op =) deps1
>>>   in (deps1, deps2) end;
>>>
>>> In particular, if sym = ccc, instead of having deps1 = [C] and deps2 =
>>> [B], we now have deps1 = [C] and deps2 = [A, B].
>>>
>>>
>>> As remark, this problem does not happen when types are by default set to
>>> be publicly exported in signatures. For instance:
>>> - The semantics of @{code ...} has slightly changed since the support of
>>> @{computation}, so the generation works now correctly in recent versions
>>> of Isabelle.
>>> - Whereas code generated by export_code may fail, we can still add the
>>> option "open" for it to skip privacy in signatures.
>>>
>>> Best,
>>> Frédéric
>>>
>>>
>>>
>>> ___
>>> isabelle-dev mailing list
>>> isabelle-...@in.tum.de
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>>
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Code generation: privacy of exported types in signatures

[Florian Haftmann]

Dear Frédéric,

I cannot follow reproduce observation; using the attached theory in
Isabelle2016-1, I get

> structure Foo : sig
>   type 'a b
>   type 'a c
>   val foo : 'a b -> 'a b
> end = struct
> 
> datatype 'a a = A;
> 
> datatype 'a b = B of 'a c a
> and 'a c = C of 'a b;
> 
> fun foo x = x;
> 
> end; (*struct Foo*)

which is almost perfectly fine, apart from the superfluous 'a c export.

How does your theory and export_code statement exactly look like?

Two points to note anyway:

* This question would belong to the user (published release) rather than
the development (ongoing changes to a central code repository) mailing list.

* The implementation of code exports is an over-approximation.  This is
a known issue but not very likely to be addressed in the near future.

Cheers,
Florian


Am 09.04.2017 um 08:04 schrieb Frederic Tuong (Dr):
> Dear all,
> 
> The SML generated code of the following snippet is not well typed
> anymore since Isabelle 2014:
> 
> datatype 'a A = aaa
> datatype 'a B = bbb "'a C A"
>  and 'a C = ccc "'a B"
> 
> This is because when computing types to be marked as not private (during
> the generation of the signature of A, B and C), A has not been assigned
> as an "Opaque" type, where the constructor Opaque is defined in
> ~~/src/Tools/Code/code_namespace.ML .
> 
> One solution is to replace the function deps_of defined in line 94 of
> http://isabelle.in.tum.de/repos/isabelle/file/7dd1971b39c1/src/Tools/Code/code_namespace.ML
> by this function:
> 
> fun deps_of sym =
>   let
> val succs1 = Code_Symbol.Graph.Keys.dest o
> Code_Symbol.Graph.imm_succs gr;
> fun succs2 x = Code_Symbol.Graph.all_succs gr [x];
> val deps1 = succs1 sym;
> val deps2 = [] |> fold (union (op =)) (map succs2 deps1) |>
> subtract (op =) deps1
>   in (deps1, deps2) end;
> 
> In particular, if sym = ccc, instead of having deps1 = [C] and deps2 =
> [B], we now have deps1 = [C] and deps2 = [A, B].
> 
> 
> As remark, this problem does not happen when types are by default set to
> be publicly exported in signatures. For instance:
> - The semantics of @{code ...} has slightly changed since the support of
> @{computation}, so the generation works now correctly in recent versions
> of Isabelle.
> - Whereas code generated by export_code may fail, we can still add the
> option "open" for it to skip privacy in signatures.
> 
> Best,
> Frédéric
> 
> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de


Foo.thy
Description: application/extension-thy


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

Re: [isabelle-dev] Irrefutable patterns in Haskell and Quickcheck/Narrowing

[Florian Haftmann]

For the record:

Lukas and me have resolved that issue in 721feefce9c6.

Cheers,
Florian

Am 14.01.2017 um 09:33 schrieb Florian Haftmann:
> Hi Lukas,
> 
> I am currently stuck with a problem in Quickcheck/Narrowing.
> 
> After about 10 years it came to surface that code generation for Haskell
> may produce irrefutable patterns due to pattern bindings in let clauses.
> See <https://wiki.haskell.org/Lazy_pattern_match>; if I understand
> <https://www.haskell.org/tutorial/patterns.html> correctly that
> particular semantics allows fancy definitions like the following
> fibonacci one-liner: »fib @ (1 : more_fib) = 1 : 1 : [ a + b | (a, b) <-
> zip fib more_fib ]«.
> 
> However the partial correctness approach of the code generator assumes
> that pattern match clauses may silently be dropped, which is made use of
> to translate the HOL-ish »partial« undefined conveniently. This breaks
> down in presence of irrefutable patterns (see the post on isabelle-users
> by Rene Thiemann).
> 
> The correction is obvious: for Haskell, only local variables may be
> bound by let clauses, but never patterns – these are solely bound by
> case clauses, which are strict in Haskell (as in function equations).
> 
> This however breaks Quickcheck/Narrowing where the lazy nature of
> pattern bindings has been exploited, may be unconsciously. A minimal
> example is attached (Quickcheck_Narrowing_Examples.thy) but I also
> distilled the generated Haskell code:
> 
> The same before and after:
>   Typerep.hs
> 
> Then the difference occurs:
>   Generated_Code.hs
>   Before: Generated_Code.A.hs
>   After: Generated_Code.B.hs
> 
> The same before and after:
>   Narrowing_Engine.hs
>   Main.hs
> 
> The diff ist straight-forward to read:
> 
>>  93,102c93,106
>>  <   let {
>>  < (Narrowing_cons (Narrowing_sum_of_products ps) cfs) = f d;
>>  < (Narrowing_cons ta cas) = a (d - (1 :: Prelude.Int));
>>  < shallow = (0 :: Prelude.Int) < d && non_empty ta;
>>  < aa = (if shallow then map (\ cf (x : xs) -> cf xs (conv cas x)) 
>> cfs
>>  <else []);
>>  <   } in Narrowing_cons
>>  <  (Narrowing_sum_of_products
>>  <(if shallow then map (\ ab -> ta : ab) ps else []))
>>  <  aa;
>>  ---
>>  >   (case f d of {
>>  > Narrowing_cons (Narrowing_sum_of_products ps) cfs ->
>>  >   (case a (d - (1 :: Prelude.Int)) of {
>>  > Narrowing_cons ta cas ->
>>  >   let {
>>  > shallow = (0 :: Prelude.Int) < d && non_empty ta;
>>  > aa = (if shallow then map (\ cf (x : xs) -> cf xs (conv 
>> cas x)) cfs
>>  >else []);
>>  >   } in Narrowing_cons
>>  >  (Narrowing_sum_of_products
>>  >(if shallow then map (\ ab -> ta : ab) ps else []))
>>  >  aa;
>>  >   });
>>  >   });
>>  112,115c116,122
>>  <   let {
>>  < (Narrowing_cons (Narrowing_sum_of_products ssa) ca) = a d;
>>  < (Narrowing_cons (Narrowing_sum_of_products ssb) cb) = b d;
>>  <   } in Narrowing_cons (Narrowing_sum_of_products (ssa ++ ssb)) (ca ++ 
>> cb);
>>  ---
>>  >   (case a d of {
>>  > Narrowing_cons (Narrowing_sum_of_products ssa) ca ->
>>  >   (case b d of {
>>  > Narrowing_cons (Narrowing_sum_of_products ssb) cb ->
>>  >   Narrowing_cons (Narrowing_sum_of_products (ssa ++ ssb)) (ca 
>> ++ cb);
>>  >   });
>>  >   });
> 
> Unfortunately my knowledge is too restricted what could be done here to
> restore the intended behaviour economically.
> 
> Hence I ask whether you have an idea what is going wrong here.
> 
> Thanks a lot!
> 
>   Florian
> 
> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

[isabelle-dev] NEWS: Computations

[Florian Haftmann]

Computations generated by the code generator can be embedded
directly into ML, alongside with @{code} antiquotations, using
the following antiquotations:

  @{computation … terms: … datatypes: …} :
((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a
  @{computation_conv … terms: … datatypes: …} :
(Proof.context -> 'ml -> conv) -> Proof.context -> conv
  @{computation_check terms: … datatypes: …} :
Proof.context -> conv

See src/HOL/ex/Computations.thy,
src/HOL/Decision_Procs/Commutative_Ring.thy and
src/HOL/Decision_Procs/Reflective_Field.thy for examples and the
tutorial on code generation.



This refers to fd753468786f and is IMHO a remarkable mile stone in the
overall code generation / reflection / proof procedure business after
more than 10 years of previous unsatisfactory attempts in that area.

The details are explained in a dedicated chapter §6 of the tutorial on
code generation.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Irrefutable patterns in Haskell and Quickcheck/Narrowing

[Florian Haftmann]

Hi Andreas,

that should be fine.  I am optimistic that we will manage somehow to
work that our during February.

Cheers,
Florian

Am 23.01.2017 um 09:39 schrieb Andreas Lochbihler:
> Hi Florian,
> 
> On 21/01/17 16:56, Florian Haftmann wrote:
>> unfortunately, a selector-based solution didn't either yield a
>> terminating example.
>>
>> If you like you can inspect the attached code, maybe I did get something
>> wrong.
>>
> I am afraid, I am busy with other stuff and won't have the time to dig
> into the details. I hope that Lukas will be able to find out what is
> going wrong.
> 
> Andreas
> 
>> I will resonsider this in approx. one week; maybe we have to raise the
>> question seriously how maintenance of quickcheck/narrowing can go on.
>>
>> Cheers,
>> Florian
>>
>> Am 14.01.2017 um 10:03 schrieb Andreas Lochbihler:
>>> Hi Florian,
>>>
>>> Lukas may be able to answer this question better, but here's a comment:
>>> You do not need the lazy treatment of irrefutable patterns in Haskell as
>>> a primitive, because it is easy to emulate using selectors. That is, if
>>> we have a single-constructor HOL datatype
>>>
>>> dataype 'a T = C (s1: 'a) (s2: 'a T) (s3: 'a T list)
>>>
>>> then we can introduce a copy of the case operator by
>>>
>>> definition case_lazy_T where "case_lazy_T = case_T"
>>> lemma [code]: "case_lazy_T f x = f (s1 x) (s2 x) (s3 x)"
>>>
>>> Now, when you want to use the semantics of irrefutable patterns in
>>> let-bindings, use case_lazy_T in the code equation. If you really want
>>> to force the evaluation, then use case_T and compile it with the new
>>> scheme.
>>>
>>> I have not tried this, but my guess is that if you do it this way for
>>> the three types narrowing_type narrowing_term narrowing_cons of
>>> Quickcheck_Narrowing and adjust the code equations for the constants in
>>> Quickcheck_Narrowing accordingly, then you get back the old behaviour.
>>>
>>> Hope this helps,
>>> Andreas
>>>
>>> On 14/01/17 09:33, Florian Haftmann wrote:
>>>> Hi Lukas,
>>>>
>>>> I am currently stuck with a problem in Quickcheck/Narrowing.
>>>>
>>>> After about 10 years it came to surface that code generation for
>>>> Haskell
>>>> may produce irrefutable patterns due to pattern bindings in let
>>>> clauses.
>>>> See <https://wiki.haskell.org/Lazy_pattern_match>; if I understand
>>>> <https://www.haskell.org/tutorial/patterns.html> correctly that
>>>> particular semantics allows fancy definitions like the following
>>>> fibonacci one-liner: »fib @ (1 : more_fib) = 1 : 1 : [ a + b | (a,
>>>> b) <-
>>>> zip fib more_fib ]«.
>>>>
>>>> However the partial correctness approach of the code generator assumes
>>>> that pattern match clauses may silently be dropped, which is made
>>>> use of
>>>> to translate the HOL-ish »partial« undefined conveniently. This breaks
>>>> down in presence of irrefutable patterns (see the post on
>>>> isabelle-users
>>>> by Rene Thiemann).
>>>>
>>>> The correction is obvious: for Haskell, only local variables may be
>>>> bound by let clauses, but never patterns – these are solely bound by
>>>> case clauses, which are strict in Haskell (as in function equations).
>>>>
>>>> This however breaks Quickcheck/Narrowing where the lazy nature of
>>>> pattern bindings has been exploited, may be unconsciously. A minimal
>>>> example is attached (Quickcheck_Narrowing_Examples.thy) but I also
>>>> distilled the generated Haskell code:
>>>>
>>>> The same before and after:
>>>> Typerep.hs
>>>>
>>>> Then the difference occurs:
>>>> Generated_Code.hs
>>>> Before: Generated_Code.A.hs
>>>> After: Generated_Code.B.hs
>>>>
>>>> The same before and after:
>>>> Narrowing_Engine.hs
>>>> Main.hs
>>>>
>>>> The diff ist straight-forward to read:
>>>>
>>>>> 93,102c93,106
>>>>> <   let {
>>>>> < (Narrowing_cons (Narrowing_sum_of_products ps) cfs) = f d;
>>>>> < (Narrowing_cons ta cas) = a (d - (1 :: Prelude.Int));
>>>>> < 

[isabelle-dev] A note on composition in src/Pure/library.ML

[Florian Haftmann]

Hi all,

in http://isabelle.in.tum.de/repos/isabelle/rev/18a6b96f8b00 you see the
result of a struggle ongoing for years now to get static vs. dynamic
scoping of code generator conversions etc. right.

Finally I realized that composition is to blame for. See the following
example:

ML_val ‹
fun foo k = error (string_of_int (k + 1));

val bar = I oo foo;

val _ = bar 41;
›

Surprisingly (?), there is no error here. The reason is obvious when
inspecting src/Pure/library.ML:

ML ‹
fun (f oo g) x y = f (g x y);
fun (f ooo g) x y z = f (g x y z);
fun (f  g) x y z w = f (g x y z w);
›

The composition operators always wait for all arguments to be applied!
Alternative definitions would be

ML ‹
fun (f oo g) x = f o g x;
fun (f ooo g) x  = f oo g x;
fun (f  g) x = f ooo g x;
›

ML_val ‹
fun foo k = error (string_of_int (k + 1));

val bar = I oo foo;

val _ = bar 41;
›

Yielding the expected error.

I am not sure whether this is a striking argument to change such
long-standing definitions dating back to c755dfd02509 in 1998. But it is
at least worth noting that these are not apt for partial application.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Irrefutable patterns in Haskell and Quickcheck/Narrowing

[Florian Haftmann]

Hi Lukas,

thanks for the offer.  We have still time before the next release to
work that out.  Just give me a sign when you start to dig into this.

All the best,
Florian


Am 21.01.2017 um 18:33 schrieb Lukas Bulwahn:
> Hi Florian,
> 
> I have been quite busy the last few days and hence did find the time
> to answer you email quickly.
> 
>> This however breaks Quickcheck/Narrowing where the lazy nature of
>> pattern bindings has been exploited, may be unconsciously. A minimal
>> example is attached (Quickcheck_Narrowing_Examples.thy) but I also
>> distilled the generated Haskell code:
> 
> Quickcheck Narrowing inherently uses Haskell's lazy evaluation to have
> a evaluation engine that implements narrowing without actually
> transforming the program that is evaluated.
> 
> The real ideas how to implement narrowing in Haskell come from the
> original authors of LazySmallCheck; the main contribution to make this
> possible in Isabelle is largely the engineering question how to
> combine the ideas from LazySmallCheck with the Isabelle code
> generator. As I was investigating this, I did some further extensions
> to allow existential quantifiers, but this is technically not that
> difficult to implement.
> 
> There is a bit of documentation describing the implementation in my thesis.
> At the moment, I am a little bit busy, but hopefully mid of February,
> I could assist looking into this.
> 
> Maintaining Quickcheck Narrowing has not been a major tasks in the
> last years there was no need to change anything as tricky as the point
> that we encounter now. Hence, I would expect that maintenance will
> continue to be low, once we resolved this issue.
> 
> Lukas
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Irrefutable patterns in Haskell and Quickcheck/Narrowing

[Florian Haftmann]

Hi Andreas,

unfortunately, a selector-based solution didn't either yield a
terminating example.

If you like you can inspect the attached code, maybe I did get something
wrong.

I will resonsider this in approx. one week; maybe we have to raise the
question seriously how maintenance of quickcheck/narrowing can go on.

Cheers,
Florian

Am 14.01.2017 um 10:03 schrieb Andreas Lochbihler:
> Hi Florian,
> 
> Lukas may be able to answer this question better, but here's a comment:
> You do not need the lazy treatment of irrefutable patterns in Haskell as
> a primitive, because it is easy to emulate using selectors. That is, if
> we have a single-constructor HOL datatype
> 
> dataype 'a T = C (s1: 'a) (s2: 'a T) (s3: 'a T list)
> 
> then we can introduce a copy of the case operator by
> 
> definition case_lazy_T where "case_lazy_T = case_T"
> lemma [code]: "case_lazy_T f x = f (s1 x) (s2 x) (s3 x)"
> 
> Now, when you want to use the semantics of irrefutable patterns in
> let-bindings, use case_lazy_T in the code equation. If you really want
> to force the evaluation, then use case_T and compile it with the new
> scheme.
> 
> I have not tried this, but my guess is that if you do it this way for
> the three types narrowing_type narrowing_term narrowing_cons of
> Quickcheck_Narrowing and adjust the code equations for the constants in
> Quickcheck_Narrowing accordingly, then you get back the old behaviour.
> 
> Hope this helps,
> Andreas
> 
> On 14/01/17 09:33, Florian Haftmann wrote:
>> Hi Lukas,
>>
>> I am currently stuck with a problem in Quickcheck/Narrowing.
>>
>> After about 10 years it came to surface that code generation for Haskell
>> may produce irrefutable patterns due to pattern bindings in let clauses.
>> See <https://wiki.haskell.org/Lazy_pattern_match>; if I understand
>> <https://www.haskell.org/tutorial/patterns.html> correctly that
>> particular semantics allows fancy definitions like the following
>> fibonacci one-liner: »fib @ (1 : more_fib) = 1 : 1 : [ a + b | (a, b) <-
>> zip fib more_fib ]«.
>>
>> However the partial correctness approach of the code generator assumes
>> that pattern match clauses may silently be dropped, which is made use of
>> to translate the HOL-ish »partial« undefined conveniently. This breaks
>> down in presence of irrefutable patterns (see the post on isabelle-users
>> by Rene Thiemann).
>>
>> The correction is obvious: for Haskell, only local variables may be
>> bound by let clauses, but never patterns – these are solely bound by
>> case clauses, which are strict in Haskell (as in function equations).
>>
>> This however breaks Quickcheck/Narrowing where the lazy nature of
>> pattern bindings has been exploited, may be unconsciously. A minimal
>> example is attached (Quickcheck_Narrowing_Examples.thy) but I also
>> distilled the generated Haskell code:
>>
>> The same before and after:
>> Typerep.hs
>>
>> Then the difference occurs:
>> Generated_Code.hs
>> Before: Generated_Code.A.hs
>> After: Generated_Code.B.hs
>>
>> The same before and after:
>> Narrowing_Engine.hs
>> Main.hs
>>
>> The diff ist straight-forward to read:
>>
>>> 93,102c93,106
>>> <   let {
>>> < (Narrowing_cons (Narrowing_sum_of_products ps) cfs) = f d;
>>> < (Narrowing_cons ta cas) = a (d - (1 :: Prelude.Int));
>>> < shallow = (0 :: Prelude.Int) < d && non_empty ta;
>>> < aa = (if shallow then map (\ cf (x : xs) -> cf xs (conv cas
>>> x)) cfs
>>> <else []);
>>> <   } in Narrowing_cons
>>> <  (Narrowing_sum_of_products
>>> <(if shallow then map (\ ab -> ta : ab) ps else []))
>>> <  aa;
>>> ---
>>> >   (case f d of {
>>> > Narrowing_cons (Narrowing_sum_of_products ps) cfs ->
>>> >   (case a (d - (1 :: Prelude.Int)) of {
>>> > Narrowing_cons ta cas ->
>>> >   let {
>>> > shallow = (0 :: Prelude.Int) < d && non_empty ta;
>>> > aa = (if shallow then map (\ cf (x : xs) -> cf xs
>>> (conv cas x)) cfs
>>> >else []);
>>> >   } in Narrowing_cons
>>> >  (Narrowing_sum_of_products
>>> >(if shallow then map (\ ab -> ta : ab) ps
>>> else []

Re: [isabelle-dev] Irrefutable patterns in Haskell and Quickcheck/Narrowing

[Florian Haftmann]

Hi Andreas,

thanks for that quick reply.  This could be done in any case, sure.

Cheers,
Florian

Am 14.01.2017 um 10:03 schrieb Andreas Lochbihler:
> Hi Florian,
> 
> Lukas may be able to answer this question better, but here's a comment:
> You do not need the lazy treatment of irrefutable patterns in Haskell as
> a primitive, because it is easy to emulate using selectors. That is, if
> we have a single-constructor HOL datatype
> 
> dataype 'a T = C (s1: 'a) (s2: 'a T) (s3: 'a T list)
> 
> then we can introduce a copy of the case operator by
> 
> definition case_lazy_T where "case_lazy_T = case_T"
> lemma [code]: "case_lazy_T f x = f (s1 x) (s2 x) (s3 x)"
> 
> Now, when you want to use the semantics of irrefutable patterns in
> let-bindings, use case_lazy_T in the code equation. If you really want
> to force the evaluation, then use case_T and compile it with the new
> scheme.
> 
> I have not tried this, but my guess is that if you do it this way for
> the three types narrowing_type narrowing_term narrowing_cons of
> Quickcheck_Narrowing and adjust the code equations for the constants in
> Quickcheck_Narrowing accordingly, then you get back the old behaviour.
> 
> Hope this helps,
> Andreas
> 
> On 14/01/17 09:33, Florian Haftmann wrote:
>> Hi Lukas,
>>
>> I am currently stuck with a problem in Quickcheck/Narrowing.
>>
>> After about 10 years it came to surface that code generation for Haskell
>> may produce irrefutable patterns due to pattern bindings in let clauses.
>> See <https://wiki.haskell.org/Lazy_pattern_match>; if I understand
>> <https://www.haskell.org/tutorial/patterns.html> correctly that
>> particular semantics allows fancy definitions like the following
>> fibonacci one-liner: »fib @ (1 : more_fib) = 1 : 1 : [ a + b | (a, b) <-
>> zip fib more_fib ]«.
>>
>> However the partial correctness approach of the code generator assumes
>> that pattern match clauses may silently be dropped, which is made use of
>> to translate the HOL-ish »partial« undefined conveniently. This breaks
>> down in presence of irrefutable patterns (see the post on isabelle-users
>> by Rene Thiemann).
>>
>> The correction is obvious: for Haskell, only local variables may be
>> bound by let clauses, but never patterns – these are solely bound by
>> case clauses, which are strict in Haskell (as in function equations).
>>
>> This however breaks Quickcheck/Narrowing where the lazy nature of
>> pattern bindings has been exploited, may be unconsciously. A minimal
>> example is attached (Quickcheck_Narrowing_Examples.thy) but I also
>> distilled the generated Haskell code:
>>
>> The same before and after:
>> Typerep.hs
>>
>> Then the difference occurs:
>> Generated_Code.hs
>> Before: Generated_Code.A.hs
>> After: Generated_Code.B.hs
>>
>> The same before and after:
>> Narrowing_Engine.hs
>> Main.hs
>>
>> The diff ist straight-forward to read:
>>
>>> 93,102c93,106
>>> <   let {
>>> < (Narrowing_cons (Narrowing_sum_of_products ps) cfs) = f d;
>>> < (Narrowing_cons ta cas) = a (d - (1 :: Prelude.Int));
>>> < shallow = (0 :: Prelude.Int) < d && non_empty ta;
>>> < aa = (if shallow then map (\ cf (x : xs) -> cf xs (conv cas
>>> x)) cfs
>>> <else []);
>>> <   } in Narrowing_cons
>>> <  (Narrowing_sum_of_products
>>> <(if shallow then map (\ ab -> ta : ab) ps else []))
>>> <  aa;
>>> ---
>>> >   (case f d of {
>>> > Narrowing_cons (Narrowing_sum_of_products ps) cfs ->
>>> >   (case a (d - (1 :: Prelude.Int)) of {
>>> > Narrowing_cons ta cas ->
>>> >   let {
>>> > shallow = (0 :: Prelude.Int) < d && non_empty ta;
>>> > aa = (if shallow then map (\ cf (x : xs) -> cf xs
>>> (conv cas x)) cfs
>>> >else []);
>>> >   } in Narrowing_cons
>>> >  (Narrowing_sum_of_products
>>> >(if shallow then map (\ ab -> ta : ab) ps
>>> else []))
>>> >  aa;
>>> >   });
>>> >   });
>>> 112,115c116,122
>>> <   let {
>>> < (Narrowing_cons (N

[isabelle-dev] Irrefutable patterns in Haskell and Quickcheck/Narrowing

[Florian Haftmann]

Hi Lukas,

I am currently stuck with a problem in Quickcheck/Narrowing.

After about 10 years it came to surface that code generation for Haskell
may produce irrefutable patterns due to pattern bindings in let clauses.
See ; if I understand
 correctly that
particular semantics allows fancy definitions like the following
fibonacci one-liner: »fib @ (1 : more_fib) = 1 : 1 : [ a + b | (a, b) <-
zip fib more_fib ]«.

However the partial correctness approach of the code generator assumes
that pattern match clauses may silently be dropped, which is made use of
to translate the HOL-ish »partial« undefined conveniently. This breaks
down in presence of irrefutable patterns (see the post on isabelle-users
by Rene Thiemann).

The correction is obvious: for Haskell, only local variables may be
bound by let clauses, but never patterns – these are solely bound by
case clauses, which are strict in Haskell (as in function equations).

This however breaks Quickcheck/Narrowing where the lazy nature of
pattern bindings has been exploited, may be unconsciously. A minimal
example is attached (Quickcheck_Narrowing_Examples.thy) but I also
distilled the generated Haskell code:

The same before and after:
Typerep.hs

Then the difference occurs:
Generated_Code.hs
Before: Generated_Code.A.hs
After: Generated_Code.B.hs

The same before and after:
Narrowing_Engine.hs
Main.hs

The diff ist straight-forward to read:

>   93,102c93,106
>   <   let {
>   < (Narrowing_cons (Narrowing_sum_of_products ps) cfs) = f d;
>   < (Narrowing_cons ta cas) = a (d - (1 :: Prelude.Int));
>   < shallow = (0 :: Prelude.Int) < d && non_empty ta;
>   < aa = (if shallow then map (\ cf (x : xs) -> cf xs (conv cas x)) 
> cfs
>      <   } in Narrowing_cons
>   <  (Narrowing_sum_of_products
>   <(if shallow then map (\ ab -> ta : ab) ps else []))
>   <  aa;
>   ---
>   >   (case f d of {
>   > Narrowing_cons (Narrowing_sum_of_products ps) cfs ->
>   >   (case a (d - (1 :: Prelude.Int)) of {
>   > Narrowing_cons ta cas ->
>   >   let {
>   > shallow = (0 :: Prelude.Int) < d && non_empty ta;
>   > aa = (if shallow then map (\ cf (x : xs) -> cf xs (conv 
> cas x)) cfs
>   >else []);
>   >   } in Narrowing_cons
>   >  (Narrowing_sum_of_products
>   >(if shallow then map (\ ab -> ta : ab) ps else []))
>   >  aa;
>   >   });
>   >   });
>   112,115c116,122
>   <   let {
>   < (Narrowing_cons (Narrowing_sum_of_products ssa) ca) = a d;
>   < (Narrowing_cons (Narrowing_sum_of_products ssb) cb) = b d;
>   <   } in Narrowing_cons (Narrowing_sum_of_products (ssa ++ ssb)) (ca ++ 
> cb);
>   ---
>   >   (case a d of {
>   > Narrowing_cons (Narrowing_sum_of_products ssa) ca ->
>   >   (case b d of {
>   > Narrowing_cons (Narrowing_sum_of_products ssb) cb ->
>   >   Narrowing_cons (Narrowing_sum_of_products (ssa ++ ssb)) (ca 
> ++ cb);
>   >   });
>   >   });

Unfortunately my knowledge is too restricted what could be done here to
restore the intended behaviour economically.

Hence I ask whether you have an idea what is going wrong here.

Thanks a lot!

Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de


Quickcheck_Narrowing_Examples.thy
Description: application/extension-thy
module
  Generated_Code(Narrowing_type(..), Narrowing_term(..), Term(..), Itself(..),
  Typerepa(..), Partial_term_of(..), Is_testable(..),
  Narrowing_cons(..), Narrowing(..), Term_of(..), Num(..),
  Char(..), Nat(..), typerep_nat, term_of_nat, non_empty, conv,
  apply, cons, sum, narrowing_nat, partial_term_of_nat,
  typerep_bool, narrowing_bool, partial_term_of_bool,
  narrowing_dummy_partial_term_of, narrowing_dummy_narrowing,
  ensure_testable, equal_nat, value)
  where {

import Prelude ((==), (/=), (<), (<=), (>=), (>), (+), (-), (*), (/), (**),
  (>>=), (>>), (=<<), (&&), (||), (^), (^^), (.), ($), ($!), (++), (!!), Eq,
  error, id, return, not, fst, snd, map, filter, concat, concatMap, reverse,
  zip, null, takeWhile, dropWhile, all, any, Integer, negate, abs, divMod,
  String, Bool(True, False), Maybe(Nothing, Just));
import qualified Prelude;
import qualified Typerep;

newtype Narrowing_type = Narrowing_sum_of_products [[Narrowing_type]];

data Narrowing_term = Narrowing_variable [Prelude.Int] Narrowing_type
  | Narrowing_constructor Prelude.Int [Narrowing_term];

data Term = Const String 

Re: [isabelle-dev] [isabelle] char :: full_exhaustive

[Florian Haftmann]

Hi Lars,

thanks for pointing this out, this was a serious slip in my work.

See now http://isabelle.in.tum.de/repos/isabelle/rev/f77b946d18aa

Cheers,
Florian

Am 20.12.2016 um 17:50 schrieb Lars Hupel:
> Dear Florian,
> 
> you changed the representation of characters a while back, but it seems
> like the Quickcheck setup is lacking a "full_exhaustive" instance.
> 
> The stupidest possible workaround is
> 
>   quickcheck_generator char constructors: char_of_nat
> 
> ... which I have just added locally to my theories.
> 
> Maybe we should think about a proper implementation.
> 
> Cheers
> Lars
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] NEWS: isabelle jedit -R

[Florian Haftmann]

Great!

Am 18.12.2016 um 22:01 schrieb Makarius:
> *** Prover IDE -- Isabelle/Scala/jEdit ***
> 
> * Command-line invocation "isabelle jedit -R -l LOGIC" opens the ROOT
> entry of the specified logic session in the editor, while its parent is
> used for formal checking.
> 
> 
> This refers to Isabelle/8edca3465758.
> 
> It facilitates maintenance of a broken session, by moving the Prover IDE
> quickly to relevant source files.
> 
> Example: isabelle jedit -R -l Collections -d '$AFP'
> 
> 
>   Makarius
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

[isabelle-dev] SysErr when using experimental polyml-test-8529546198aa in JinjaThreads

[Florian Haftmann]

> isabelle: c48becd96398 tip
> afp: 45dd81cdecef tip
> Building HOL ...
> Finished HOL (0:01:56 elapsed time, 0:05:46 cpu time, factor 2.97)
> Building HOL-Word ...
> Finished HOL-Word (0:00:14 elapsed time, 0:00:40 cpu time, factor 2.74)
> Building JinjaThreads ...
> JinjaThreads FAILED
> (see also 
> /srv/data/tum/isabelle/devel/heaps/polyml-5.6_x86-linux/log/JinjaThreads)
>  list
>  *
>  (Isabelle8115590.Generated_Code.nat *
>   (Isabelle8115590.Generated_Code.nat * (string option * ...))
>  )
>  list))
>*
>(Isabelle8115590.Generated_Code.nat
> Isabelle8115590.Generated_Code.vala
> list
> *
> (Isabelle8115590.Generated_Code.nat
>  Isabelle8115590.Generated_Code.vala
>  list
>  *
>  (string * (string * Isabelle8115590.Generated_Code.nat
>   )
>   list)
>  *
>  (Isabelle8115590.Generated_Code.nat, Isabelle8115590.Generated_Code.nat
>  )
>  Isabelle8115590.Generated_Code.finfun
>  )
>  Isabelle8115590.Generated_Code.rbt
>  *
>  (Isabelle8115590.Generated_Code.nat,
>  Isabelle8115590.Generated_Code.heapobj)
>  Isabelle8115590.Generated_Code.rbt)
> *
> ((Isabelle8115590.Generated_Code.nat,
>  Isabelle8115590.Generated_Code.nat
>  Isabelle8115590.Generated_Code.wait_set_status
>  )
>  Isabelle8115590.Generated_Code.rbt
>  *
>  (Isabelle8115590.Generated_Code.nat, unit)
>  Isabelle8115590.Generated_Code.rbt))
>)
>Isabelle8115590.Generated_Code.tllist
> *** exception SysErr ("Cannot allocate memory", SOME ENOMEM) raised (line 83 
> of "./basis/PolyMLException.sml")
> Unfinished session(s): JinjaThreads
> 0:32:24 elapsed time, 1:54:58 cpu time, factor 3.55

JinjaThreads with regular PolyML finishes within about 30 minutes.

Relevant hardware data might include:

> $ lscpu
> Architecture:  x86_64
> CPU op-mode(s):32-bit, 64-bit
> Byte Order:Little Endian
> CPU(s):8
> On-line CPU(s) list:   0-7
> Thread(s) pro Kern:2
> Kern(e) pro Socket:4
> Socket(s): 1
> NUMA-Knoten:   1
> Anbieterkennung:   GenuineIntel
> Prozessorfamilie:  6
> Modell:94
> Model name:Intel(R) Core(TM) i7-6700K CPU @ 4.00GHz
> Stepping:  3
> CPU MHz:   800.000
> CPU max MHz:   4200,
> CPU min MHz:   800,
> BogoMIPS:  8015.87
> Virtualisierung:   VT-x
> L1d Cache: 32K
> L1i Cache: 32K
> L2 Cache:  256K
> L3 Cache:  8192K
> NUMA node0 CPU(s): 0-7
> Flags: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge 
> mca cmov pat pse36 clflush dts acpi mmx fxsr sse sse2 ss ht tm pbe syscall nx 
> pdpe1gb rdtscp lm constant_tsc art arch_perfmon pebs bts rep_good nopl 
> xtopology nonstop_tsc aperfmperf eagerfpu pni pclmulqdq dtes64 monitor ds_cpl 
> vmx est tm2 ssse3 sdbg fma cx16 xtpr pdcm pcid sse4_1 sse4_2 x2apic movbe 
> popcnt tsc_deadline_timer aes xsave avx f16c rdrand lahf_lm abm 3dnowprefetch 
> epb intel_pt tpr_shadow vnmi flexpriority ept vpid fsgsbase tsc_adjust bmi1 
> hle avx2 smep bmi2 erms invpcid rtm mpx rdseed adx smap clflushopt xsaveopt 
> xsavec xgetbv1 dtherm ida arat pln pts hwp hwp_notify hwp_act_window hwp_epp

> $ free
>   totalusedfree  shared  buff/cache   
> available
> Mem:   16099596 135539612329292  265960 2414908
> 14110560
> Swap:   8388604   0 8388604

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_at_haftmann_online_de.pgp



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

[isabelle-dev] Failure in AFP when switching from polyml-5.6-1 to polyml-test-7a7b742897e9

[Florian Haftmann]

Hi all,

when testing polyml-test-7a7b742897e9 I found out that this breaks
session Algebraic_Numbers in the AFP:

*** At command "value" (line 42 of
"/mnt/home/haftmann/data/tum/afp/devel/thys/Algebraic_Numbers/Algebraic_Number_Tests.thy")
*** exception Div raised (line 302 of "./basis/InitialBasis.ML")

It looks like a change in the semantics of integer division in PolyML,
but this is entirely speculative.

The corresponding HG ids are near
Isabelle: 3d4331b65861
AFP:  74c0b7f55fa2

Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

[isabelle-dev] AFP broken

[Florian Haftmann]

> isabelle: ae7c11573922 tip
> afp: 1bffa6708aea tip
> *** [line 5 of 
> "/mnt/home/haftmann/data/tum/afp/master/thys/SPARCv8/lib/WordDecl.thy"] 
> error: command "theory" expected,
> *** but identifier was found:
> *** header
> *** 
> *** 
> *** ^
> *** The error(s) above occurred for theory "WordDecl" (line 3 of 
> "/mnt/home/haftmann/data/tum/afp/master/thys/SPARCv8/ROOT")
> *** [line 11 of 
> "/mnt/home/haftmann/data/tum/afp/master/thys/SPARCv8/SparcModel_MMU/Sparc_Instruction.thy"]
>  error: command "theory" expected,
> *** but identifier was found:
> *** header
> *** 
> *** 
> *** ^
> *** The error(s) above occurred for theory "Sparc_Instruction"
> *** (required by "Sparc_Properties" via "Sparc_Execution") (line 12 of 
> "/mnt/home/haftmann/data/tum/afp/master/thys/SPARCv8/SparcModel_MMU/Sparc_Execution.thy")
> *** [line 11 of 
> "/mnt/home/haftmann/data/tum/afp/master/thys/SPARCv8/SparcModel_MMU/Sparc_State.thy"]
>  error: command "theory" expected,
> *** but identifier was found:
> *** header
> *** 
> *** 
> *** ^
> *** The error(s) above occurred for theory "Sparc_State"
> *** (required by "Sparc_Properties" via "Sparc_Execution") (line 12 of 
> "/mnt/home/haftmann/data/tum/afp/master/thys/SPARCv8/SparcModel_MMU/Sparc_Execution.thy")
> *** [line 11 of 
> "/mnt/home/haftmann/data/tum/afp/master/thys/SPARCv8/SparcModel_MMU/Sparc_Types.thy"]
>  error: command "theory" expected,
> *** but identifier was found:
> *** header
> *** 
> *** 
> *** ^
> *** The error(s) above occurred for theory "Sparc_Types"
> *** (required by "Sparc_Properties" via "Sparc_Execution") (line 12 of 
> "/mnt/home/haftmann/data/tum/afp/master/thys/SPARCv8/SparcModel_MMU/Sparc_Execution.thy")
> *** The error(s) above occurred in session "SPARCv8" (line 3 of 
> "/mnt/home/haftmann/data/tum/afp/master/thys/SPARCv8/ROOT")



-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

[isabelle-dev] Distro broken

[Florian Haftmann]

> isabelle: fb5c74a58796 tip
> afp: c03838321f2a tip
> *** No such file: 
> "/mnt/home/haftmann/data/tum/isabelle/devel/src/HOL/Probability/Essential_Supremum.thy"
> *** The error(s) above occurred for theory "Essential_Supremum"
> *** (required by "Probability") (line 15 of 
> "/mnt/home/haftmann/data/tum/isabelle/devel/src/HOL/Probability/Probability.thy")
> *** The error(s) above occurred in session "HOL-Probability" (line 716 of 
> "/mnt/home/haftmann/data/tum/isabelle/devel/src/HOL/ROOT")

Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Old_Number_Theory

[Florian Haftmann]

Hi Manuel,

> I am glad to announce that as of261d42f0bfac, Old_Number_Theory is
> finally history.

these are good news indeed.

One remark on the diff:

+ src/HOL/Number_Theory/QuadraticReciprocity.thy
+ src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy

This is a formal regression: a proper name has turned into CaMlCaSe.
But that should be easy to correct.

There is another pre-existing CaMlCaSe theory, MiscAlgebra; but from the
description of the theory itself this should go suitable HOL-Algebra
theories anyway.

> A lot of the proofs are still quite messy and don't take advantage of
> the new features we now have in Number_Theory (such as a uniform concept
> of ‘primes’ and ‘prime factorisations’ for both nat and int), but I do
> not think the work necessary to achieve that is worth it.

Messy proofs can be amended in case of need.  Messy definitions are more
critical since they may infect further theories, but all that seems to
have disappeared in the transition.

> The vast majority of the porting work was done by a student of ours,
> Jaime Mendizabal Roche, so big thanks to him. He even extended the ‘two
> squares’ AFP entry a bit, showing the converse direction as well.

Thanks a lot also!

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Towards the release

[Florian Haftmann]

> Are there any non-trivial chunks still in the commit/push pipeline that
> need special considerations?

I have some matter on euclidean division in the pipeline which I hope to
be able to finish before my vacation starting at end of October.

Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Jenkins maintenance

[Florian Haftmann]

> Also note that the Mira architects were actually looking at Jenkins at
> that time, and pointed out that it was a bit old-fashioned in focusing
> on "latest" versions by default and lacking proper changeset identification.

The story behind is actually more delicate:  mira was started with the
following intentions:
a) provide a replacement for the isatest infrastructure with its
uncertain future at that time;
b) separate the »general idea« from the concrete application;
c) explore the design space for scheduling tests covering and combining
multiple histories.

The incentive to pursue c) led us to ignore Hudson/Jenkins entirely,
with the attitude »keep it simple, stupid«.

The following insights contributed to abandon the project:

1) Over time it became manifest that c) is too ambitious wrt. real
existing resources, hence the insight that pragmatically »tip testing«
is not so bad at all.

2) Further, »keep it simple, stupid« came to its limits with all the
involved technicalities: issues jobs on remote machines, exception
handling, proper daemonizing – it is surely easy to extend that list.
The Jenkins universe, as fas as I can tell, embodies significant
expertise in that area which you don't want to reimplement.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] [isabelle] Reconciling FinFuns in Distro and AFP

[Florian Haftmann]

See now #55256a98f65f.

The proofs are really a challenge…

Am 16.09.2016 um 22:29 schrieb Lars Hupel:
>> This is already ongoing. Johannes and Fabian agreed to replacing the
>> finite maps in HOL-Probability with a new representation (cf
>> a4acecf4dc21), which will shortly appear in HOL-Library (it's not high
>> priority though).
> 
> See now Isabelle/2359e9952641. This contains some initial code setup
> which should be enough for most purposes; it uses "AList" underneath.
> 
> There is a prime candidate for consolidation in the AFP (see
> "Finite_Map2" theory), which I attempted to port, but then "back"ed out
> (literally – there is a proof with over 10 "back" statements which I
> would've had to fix). In case anyone is particularly adventurous, feel
> free to go ahead ...
> 
> Cheers
> Lars
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

[isabelle-dev] Theory for discrete log etc.

[Florian Haftmann]

Hi all,

after studying 28d1deca302e I realized that we have now two theories
dealing with discrete functions (with one having been hidden in
Float.thy for years):

  Log_Nat.floorlog :: "nat ⇒ nat ⇒ nat"
  Discrete.log :: "nat ⇒ nat"
  Log_Nat.bitlen :: "int ⇒ int"
  Discrete.sqrt :: "nat ⇒ nat"

»Discrete.log« seems to be »Log_Nat.floorlog 2« and »Log_Nat.bitlen« is
just a variant with different types.

Just to place a memo for future consolidation.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] comm_monoid, comm_monoid_set in bbcb05504fdc

[Florian Haftmann]

See now 7faa9bf9860b for a related issue.

We had a personal conversation that it is very likely that the remaning
issues will disappear after the next big envisaged reform of the
analysis material.

Cheers,
Florian

Am 07.08.2016 um 10:47 schrieb Florian Haftmann:
> Hi Johannes,
> 
> that change had probably more pervasive effects than intended.  E.g. the
> definition
> 
> definition (in comm_monoid) operative …
> 
> and its basic lemmas now produce the following soup of theorems
> 
> thm inf_top.operative_def sup_bot.operative_def add.operative_def
> mult.operative_def gcd_nat.operative_def inf_top.operativeD
> sup_bot.operativeD add.operativeD mult.operativeD gcd_nat.operativeD
> inf_top.operative_empty sup_bot.operative_empty add.operative_empty
> mult.operative_empty gcd_nat.operative_empty add.comm_monoid_lift_option
> mult.comm_monoid_lift_option inf_top.comm_monoid_lift_option
> sup_bot.comm_monoid_lift_option gcd_nat.comm_monoid_lift_option
> 
> I will be in Garching on Tue and have already some ideas in the pocket
> how to improve that which we could discuss then.
> 
> Cheers,
>   Florian
> 
> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] [isabelle] Proposal: An update to Multiset theory

[Florian Haftmann]

See now rev. 76302202a92d

Thanks for contributing!

Cheers,
Florian

Am 08.08.2016 um 14:44 schrieb Bertram Felgenhauer:
> Florian Haftmann wrote:
>> Hi Bertram,
>>
>>> How shall we proceed? As I hinted at earlier I do not have (nor want, at
>>> this point) push access, but I can prepare a patch or clone of the repo,
>>> if that helps, or just provide a plain theory file that works with the
>>> development version of Isabelle.
>>
>> a repo URL or a patch is indeed the best thing to proceed: there is not
>> »the« development version but an ongoing agile development.
> 
> Okay, I have exported a series of two patches against 1e7c5bbea36d,
> the first adding monotonicity lemmata and the second for cancellation
> and `multp`, `multeq`. See the attached file.
> 
> Cheers,
> 
> Bertram
> 
> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

[isabelle-dev] comm_monoid, comm_monoid_set in bbcb05504fdc

[Florian Haftmann]

Hi Johannes,

that change had probably more pervasive effects than intended.  E.g. the
definition

definition (in comm_monoid) operative …

and its basic lemmas now produce the following soup of theorems

thm inf_top.operative_def sup_bot.operative_def add.operative_def
mult.operative_def gcd_nat.operative_def inf_top.operativeD
sup_bot.operativeD add.operativeD mult.operativeD gcd_nat.operativeD
inf_top.operative_empty sup_bot.operative_empty add.operative_empty
mult.operative_empty gcd_nat.operative_empty add.comm_monoid_lift_option
mult.comm_monoid_lift_option inf_top.comm_monoid_lift_option
sup_bot.comm_monoid_lift_option gcd_nat.comm_monoid_lift_option

I will be in Garching on Tue and have already some ideas in the pocket
how to improve that which we could discuss then.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_at_haftmann_online_de.pgp



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

Re: [isabelle-dev] Multiset insert

[Florian Haftmann]

Just an aside: concerning »insert« and »add«, infix syntax would be
desirable, e.g.

a `insert` X
a `add` M


similar to

Y \union Y
N + M

which would yield much more readable propositions, esp. wrt. associativity:

a `insert` b `insert` X = {a, b} \union X
vs.
insert a (insert b X) = {a, b} \union X

This is structurally similar to append and cons on lists:

x # y # xs = [x, y] @ xs

But so far I have seen any convincing symbolic notation for that for
sets or multisets.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Multiset insert

[Florian Haftmann]

>> Tobias wrote:
>>
>>> How about
>>>
>>> definition add_mset :: "'a ⇒ 'a multiset ⇒ 'a multiset" ("add#") where
>>> "add# x M = {#x#} + M"
> 
> This, however, may produce confusion with multiset union, which is an
> instance of the plus type classes, i.e., occupying the name
> plus_multiset.

To a certain extent, maybe.  The plus type class has (among other
syntactic type classes) the historic defect that type class and
operation are named »plus« whereas properties refer to »add«.  To which
I have contributed since I chose »plus« etc. when giving those
operations proper names back in 2005 / 2006 / 2007.

However this is maybe now all too depp-rooted to consolidate it.  Even
if not, alternatives have been proposed here that would resolve that
issue than.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] {0::nat..<n} = {..<n}

[Florian Haftmann]

> The whole setup has grown over time and initially I may have preferred
> {..<n} just like you did. I would welcome your proposed changes.

See now c184ec919c70.

The core addition are substantial theorems concerning indexed sums and
products, using locale comm_monoid_set to provide them uniformly for
setsum and setprod.

I still hesitated to add suitable default simp rules.  Let's see…

Cheers,
Florian

> 
> I agree, sums look nicer with {..<n}, but look at the bright side:
> {0..<n} clearly shows that the set/sum is bounded, something that is
> otherwise implicit in the type.
> 
> Tobias
> 
> On 04/07/2016 21:00, Florian Haftmann wrote:
>>> The problem with {..<n} on nat is that you need multiple versions of
>>> every lemma involving {m..<n} on nat. Hence I discourage the use of
>>> {..<n} on nat. If you add ‹{0..<n} = {..<n}› it will solve many but not
>>> all problems: not all proof methods invoke simp all the time.
>>>
>>> I consider {..<n} on nat an anomaly that should be avoided because one
>>> gains very little by using it. One could even think aout replacing it by
>>> {0..<n} upon parsing.
>>
>> OK, then {0..<n} is the canonical representative.  And, as I did not
>> realize before, rules concerning {0..> to state as rules concerning {..> bound.
>>
>> However then I suggest to add a few lemmas to emphasize that decision,
>> e.g.
>>
>> lemma lessThan_atLeast0:
>>   fixes n :: nat
>>   shows "{..<n} = {0..<n}"
>>   by (simp add: atLeast0LessThan)
>>
>> lemma atMost_atLeast0:
>>   fixes n :: nat
>>   shows "{..n} = {0..n}"
>>   by (simp add: atLeast0AtMost)
>>
>> Currently, only their symmetrics are present, but not these, which would
>> suggest that {..<n} is the canonical form.
>>
>> Similarly for ‹{0..> {..n}›
>>
>> What remains a little bit unsatisfactory is the printing of sums and
>> products:
>>
>> term "setsum (\n. n ^ 3) {0..<m::nat}" -- \\n =
>> 0..
>> term "setsum (\n. n ^ 3) {..<m::nat}" -- \\n> 3\
>> term "setsum (\n. n ^ 3) {0..m::nat}" -- \\n = 0..m.
>> n ^ 3\
>> term "setsum (\n. n ^ 3) {..m::nat}" -- \\n\m. n
>> ^ 3\
>>
>> Here the non-canonical forms are superior to read, but I think we can
>> live with that.
>>
>> Since I have currently laid hands-on on that matter, I would offer to
>> add lessThan_atLeast0, atMost_atLeast0 and ‹{0..> {0..n}› to the distribution.  I would also polish one or two definitions
>> in Binomial.thy which currently involve the non-canonical forms.
>>
>> Maybe lessThan_atLeast0 and atMost_atLeast0 are suitable candidates for
>> default simp rules also then.
>>
>> Cheers,
>> Florian
>>
>>>> obviously on natural numbers ‹{0..<n} = {..<n}› holds, and the right
>>>> hand side is also more convenient to work with (no preconditions on m
>>>> being less or equal n etc.). But for historic reasons, ‹{0..<n}› is
>>>> still the preferred variant in many theorems, cf. ‹find_theorems
>>>> "{0::nat..<_}"›.
>>>>
>>>> I'm tempted to say that these occurrences should be normalized to
>>>> ‹{..<n}› and ‹{0..<n} = {..<n}› be added as default simp rule, but I
>>>> leave it to experts on intervals to judge.
> 
> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Considered harmful: surj

[Florian Haftmann]

> Yes I second that. It surely is a good idea to just use it only as a
> input translation.

See now 6af79184bef3.

Florian

> 
>  - Johannes
> 
> Am Samstag, den 02.07.2016, 21:08 +0200 schrieb Florian Haftmann:
>> Hi all,
>>  
>> since cf26dd7395e4, ‹surj f› is a mere abbreviation for ‹range f =
>> UNIV›. This is a little bit unfortunate since an ordinary equation is
>> just hidden in output that way, resulting in lots of casual
>> confusion. I
>> would suggest to turn ‹surj› into a mere input abbreviation, similar
>> to
>> ‹trivial_limit› which also covers an equality. This may also open the
>> possibility to re-introduce ‹surj_on f A› as in input abbreviation
>> for
>> ‹range f = A›, which got abolished in cf26dd7395e4, leaving a strange
>> assymmetry wrt. inj(_on), bij(_betw).
>>  
>> Cheers,
>>  Florian
>>
>> ___
>> isabelle-dev mailing list
>> isabelle-...@in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
>> le-dev
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Permutations

[Florian Haftmann]

> What about adding it to the ab_group_add typeclass? I know this is not
> the usual mathematical syntax for permutations, but at least we can
> reuse a lot of theorems from this type class.

There *is* reuse since there is a separate interpretation of the
abstract ab_group locale.

I once met an algebraist who preferred + for abelian groups and *
otherwise, and this makes sense.

Cheers,
Florian


> 
>  - Johannes
> 
> Am Dienstag, den 05.07.2016, 19:40 +0200 schrieb Florian Haftmann:
>>>
>>> One question: why did you only set it up for monoid_mult and
>>> inverse,
>>> and not as a ab_group_mult?
>> The answer is simple: there is no type class
>> ab_group_mult.  Why?  Since
>> our multiplicative structures are tailored towards rings where 0 is
>> no
>> part of the multiplicative group.
>>
>> Cheers,
>>  Florian
>>

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] {0::nat..<n} = {..<n}

[Florian Haftmann]

Hello Andreas,

> AFAIU {..<n} wouldn't protect against negative integers and might
> deliver wrong positive.
> AFAIK the questionif 0 is part of natural numbers is disputed. Was there
> some solution in recent years?
> Depending on that {1..<n} might be an option too in some cases.

each value (term) in Isabelle/HOL has a type, and a type can be thought
of as a fixed (non-empty) set of values.  In this thread we have solely
talked about the type ‹nat› which corresponds to the natural numbers
including zero.

Cheers,
Florian

> 
> Cheers,
> Andreas
> 
> On 05.07.2016 08:38, Tobias Nipkow wrote:
>> Florian,
>>
>> The whole setup has grown over time and initially I may have preferred
>> {..<n} just like you did. I would welcome your proposed changes.
>>
>> I agree, sums look nicer with {..<n}, but look at the bright side:
>> {0..<n} clearly shows that the set/sum is bounded, something that is
>> otherwise implicit in the type.
>>
>> Tobias
>>
>> On 04/07/2016 21:00, Florian Haftmann wrote:
>>>> The problem with {..<n} on nat is that you need multiple versions of
>>>> every lemma involving {m..<n} on nat. Hence I discourage the use of
>>>> {..<n} on nat. If you add ‹{0..<n} = {..<n}› it will solve many but not
>>>> all problems: not all proof methods invoke simp all the time.
>>>>
>>>> I consider {..<n} on nat an anomaly that should be avoided because one
>>>> gains very little by using it. One could even think aout replacing
>>>> it by
>>>> {0..<n} upon parsing.
>>>
>>> OK, then {0..<n} is the canonical representative.  And, as I did not
>>> realize before, rules concerning {0..>> to state as rules concerning {..>> bound.
>>>
>>> However then I suggest to add a few lemmas to emphasize that
>>> decision, e.g.
>>>
>>> lemma lessThan_atLeast0:
>>>   fixes n :: nat
>>>   shows "{..<n} = {0..<n}"
>>>   by (simp add: atLeast0LessThan)
>>>
>>> lemma atMost_atLeast0:
>>>   fixes n :: nat
>>>   shows "{..n} = {0..n}"
>>>   by (simp add: atLeast0AtMost)
>>>
>>> Currently, only their symmetrics are present, but not these, which would
>>> suggest that {..<n} is the canonical form.
>>>
>>> Similarly for ‹{0..>> {..n}›
>>>
>>> What remains a little bit unsatisfactory is the printing of sums and
>>> products:
>>>
>>> term "setsum (\n. n ^ 3) {0..<m::nat}" -- \\n =
>>> 0..
>>> term "setsum (\n. n ^ 3) {..<m::nat}" -- \\n>> 3\
>>> term "setsum (\n. n ^ 3) {0..m::nat}" -- \\n = 0..m.
>>> n ^ 3\
>>> term "setsum (\n. n ^ 3) {..m::nat}" -- \\n\m. n
>>> ^ 3\
>>>
>>> Here the non-canonical forms are superior to read, but I think we can
>>> live with that.
>>>
>>> Since I have currently laid hands-on on that matter, I would offer to
>>> add lessThan_atLeast0, atMost_atLeast0 and ‹{0..>> {0..n}› to the distribution.  I would also polish one or two definitions
>>> in Binomial.thy which currently involve the non-canonical forms.
>>>
>>> Maybe lessThan_atLeast0 and atMost_atLeast0 are suitable candidates for
>>> default simp rules also then.
>>>
>>> Cheers,
>>> Florian
>>>
>>>>> obviously on natural numbers ‹{0..<n} = {..<n}› holds, and the right
>>>>> hand side is also more convenient to work with (no preconditions on m
>>>>> being less or equal n etc.). But for historic reasons, ‹{0..<n}› is
>>>>> still the preferred variant in many theorems, cf. ‹find_theorems
>>>>> "{0::nat..<_}"›.
>>>>>
>>>>> I'm tempted to say that these occurrences should be normalized to
>>>>> ‹{..<n}› and ‹{0..<n} = {..<n}› be added as default simp rule, but I
>>>>> leave it to experts on intervals to judge.
>>
>>
>>
>> ___
>> isabelle-dev mailing list
>> isabelle-...@in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] An experience report on the testboard

[Florian Haftmann]

Am 04.07.2016 um 23:49 schrieb Lars Hupel:
>> The problem I was referring to is that in order to get a deeper idea
>> what's going on you want to have a look at the topology of the history.
>>  However I guess this is closely related to my surprise that not both
>> patches to distro and AFP pushed in proximity have been considered as
>> one build job.  So maybe this is not important.
> 
> Sorry, I don't understand. You push some changeset and Jenkins will tell
> you exactly which Mercurial id is the current tip. What else do you need?

You may ignore my confusion safely.

> Right. That would be easier under the presence of a good
> "testboard_submit" command.
> 
> As I alluded to in my earlier email this is all well within the realm of
> possibility (even platform-independent desktop notifications upon
> completion), but it requires some dedicated implementation effort.

What I see from this thread is that at some time we really have to talk
about official build orders with respective hg ids, either using
subrepos or whatever.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Permutations

[Florian Haftmann]

> One question: why did you only set it up for monoid_mult and inverse,
> and not as a ab_group_mult?

The answer is simple: there is no type class ab_group_mult.  Why?  Since
our multiplicative structures are tailored towards rings where 0 is no
part of the multiplicative group.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

[isabelle-dev] Permutations

[Florian Haftmann]

Hi all,

see 59803048b0e8 for some basic facts about almost everywhere bijections
aka permutations. Maybe this will become a convenient coagulation point
for various scattered material in the future.

It turned out quite ambitious to formulate basic properties, e.g.
circularity. I did not search for any literature because I thought that
things covered in introductory courses should be straightforward to
formalize ;-).

My original interest had been cycles, but I realized that this needs
more work than I am willing to spend here, even more since I further
realized that the combinatorial interpretation of first Stirling numbers
can work just on cycles without need of their interpretation as
permutations.

If anybody wants to push that work further, the agenda is roughly as
follows:
* Consolidate scattered material on permutations (functions) into
Library/Perm.thy (see my post
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-June/msg00091.html
for further details).
* Gradually abandon Library/Permutation with its equivalence relation
‹perm› – it is much easier to reason about equality on multisets ‹mset
xs = mset ys›. There is also no equivalence relation ‹same_elems :: 'a
list ⇒ 'a list ⇒ bool›, but we write just ‹set xs = set ys›, for the
same and good reason.

I still have some work regarding cycles and combinatorial functions in
the drawer which I hope to finish gradually over time.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

[isabelle-dev] Bijections

[Florian Haftmann]

Hi all,

in 1a474286f315 I have introduced a locale for (total) bijections,
allowing to obtain typical facts like ‹inv f ∘ f = id› by interpretation.

The motivation was that most of these facts have not ‹bij› but ‹inj› or
‹surj› as premise, which makes proof complicated due to two lifting
steps, especially if you need the same facts over and over.

Of course there could also be a locale for partial bijections, and also
a whole hierarchy spanning injections etc., but this would result in a
lot of duplication.

The idea to turn all those predicates into locales sounds too radical
for me, since lifting arguments referring to terms like ‹bij (f ∘ g)›
are tedious to express within the module system. But maybe others with
more experience than me in that area have already made some thoughts
about that matter.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] An experience report on the testboard

[Florian Haftmann]

>> 3. Go to https://ci.isabelle.systems/jenkins/job/testboard-afp/ and
>> await new build run to be scheduled.
> 
> There can currently only be one testboard build running at a time. That
> means you should wait to push until the previous run is finished.
> 
> I understand that this is not ideal. It is fixable, but not very high
> priority right now.

Well, it just means that there are no queued builds.  I agree that we
can easily live with that.

>> A disadvantage is that you have to click a lot to find out the hash id
>> in the distribution view. I guess that could be easily resolved by a
>> suitable configuration, or hosting the distribution testboard repository
>> in the same hosting environment as the AFP testboard repository.
> 
> An easier way is this: Go to  and
> on the bottom of the page, click on the appropriate testboard button. It
> will take you to an overview page of Jenkins where you can see the
> changes which triggered the build (including links to hgweb) and also
> links to the console outputs of the subjobs.

The problem I was referring to is that in order to get a deeper idea
what's going on you want to have a look at the topology of the history.
 However I guess this is closely related to my surprise that not both
patches to distro and AFP pushed in proximity have been considered as
one build job.  So maybe this is not important.

>> 5. Then repeatedly check the URI of the build until results are available.
> 
> What kind of notification would you envision here?

A notification to the committer(s) of the respective changesets.  Maybe
Jenkins has already support for that?

>> An inherent weakness of the testboard approach is that whenever you
>> gradually improve your changesets you to rebuild ab initio. But the
>> building times are compact enough that this shouldn't be too big a problem.
> 
> The new hardware brought the raw build time down to about an hour. An
> obvious optimisation would be to not clean before building. But then
> again, most often, changes being tested out affect Pure or HOL which
> means everything needs to be rebuilt anyway.

The workflow I am alluding to is as follows:
a) You make a change to the distro.
b) You have a rough idea what the consequences are and check the
involved sessions after an analysis.
c) You do some kind of plausibility checking (e.g. building HOL-Library)-
d) You push optimistically to the testboard.
e) Hence you get a rough idea what has still to be done in certain sessions.
f) You check the corresponding sessions.
g) Now you are ready for the next iteration.

As I said, I think we can live without any optimisation here at the moment.

Cheers,
Florian

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

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] An experience report on the testboard

[Florian Haftmann]

>> 1. Changesets to dist and AFP exist as hg patches.
> 
> This is currently not implemented. Isabelle testboard will always use
> AFP devel and vice versa. It is not possible to test Isabelle testboard
> and AFP testboard together.

But I regard this as a central use case: if a change to the distro
demands changes in the AFP, you want to test them simultaneously.

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] {0::nat..<n} = {..<n}

[Florian Haftmann]

> The problem with {.. every lemma involving {m.. {.. all problems: not all proof methods invoke simp all the time.
> 
> I consider {.. gains very little by using it. One could even think aout replacing it by
> {0.. obviously on natural numbers ‹{0..> hand side is also more convenient to work with (no preconditions on m
>> being less or equal n etc.). But for historic reasons, ‹{0..> still the preferred variant in many theorems, cf. ‹find_theorems
>> "{0::nat..<_}"›.
>> 
>> I'm tempted to say that these occurrences should be normalized to
>> ‹{..> leave it to experts on intervals to judge.
-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

[isabelle-dev] Considered harmful: surj

[Florian Haftmann]

Hi all,

since cf26dd7395e4, ‹surj f› is a mere abbreviation for ‹range f =
UNIV›. This is a little bit unfortunate since an ordinary equation is
just hidden in output that way, resulting in lots of casual confusion. I
would suggest to turn ‹surj› into a mere input abbreviation, similar to
‹trivial_limit› which also covers an equality. This may also open the
possibility to re-introduce ‹surj_on f A› as in input abbreviation for
‹range f = A›, which got abolished in cf26dd7395e4, leaving a strange
assymmetry wrt. inj(_on), bij(_betw).

Cheers,
Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_at_haftmann_online_de.pgp



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

[isabelle-dev] {0::nat..<n} = {..<n}

[Florian Haftmann]

Hi all,

obviously on natural numbers ‹{0..

[isabelle-dev] An experience report on the testboard

[Florian Haftmann]

Hi all,

I have started to use the testboard and want to excite feedback on my
workflow, as well as hint to certain inconveniences in the current setup.

1. Changesets to dist and AFP exist as hg patches.

2. In both repositories:
hg push_to_testboard
where »push_to_testboard« according to .hgrc is defined as
alias for
»!{ "${HG}" push -f testboard && "${HG}" phase --force --draft; }«

3. Go to https://ci.isabelle.systems/jenkins/job/testboard-afp/ and
await new build run to be scheduled.

4. Check that newly emerging build and compare the hash ids according to
http://isabelle.in.tum.de/repos/testboard/summary and
https://bitbucket.org/isa-afp/afp-testboard/commits/all

Here I encountered two problems:
* Even if pushes occur in close proximity, there is a chance that they
are not matched in that particular build.
* To resolve the situation, I did qpop and qpush, this creating patches
with different hash ids. But pushing that did not trigger a new run.
Don't know what's exactly going on here…
A disadvantage is that you have to click a lot to find out the hash id
in the distribution view. I guess that could be easily resolved by a
suitable configuration, or hosting the distribution testboard repository
in the same hosting environment as the AFP testboard repository.

5. Then repeatedly check the URI of the build until results are available.

An inherent weakness of the testboard approach is that whenever you
gradually improve your changesets you to rebuild ab initio. But the
building times are compact enough that this shouldn't be too big a problem.

Cheers,
Florian


-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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