Email Gateway (Aug 22 2022 at 16:02): Email Gateway (Aug 22 2022 at 16:02):From: "C. Diekmann" <diekmann@in.tum.de>
Dear Makarius,
I just loaded Monad_Syntax in Isabelle2017-RC1 and observed that it pulls
in many dependencies. In particular, it transitively depends
on Old_Datatype. This is not a bug, but very surprising behavior to me: I
would expect only additional syntactic sugar from a theory that calls
itself _Syntax and not a huge set of Old_ functionality.
Best,
Cornelius
Email Gateway (Aug 22 2022 at 16:03):From: Lars Hupel <hupel@in.tum.de>
That is partly my fault.
changeset: 66260:466d8e7ed170
user: Lars Hupel <lars.hupel@mytum.de>
date: Mon Jul 10 23:21:54 2017 +0200
summary: FSet is monadic
Monad_Syntax sets up sugar for finite sets, which pulls in "Countable",
which provides a tactic that works on "Old_Datatype".
A quick grep over distribution+AFP suggests that that tactic is not used
on old datatypes.
Cheers
Lars
Email Gateway (Aug 22 2022 at 16:03):From: Makarius <makarius@sketis.net>
Is there a genuine problem behind it? Otherwise I would say we leave it
like that for the release.
Makarius
Email Gateway (Aug 22 2022 at 16:03):From: "C. Diekmann" <diekmann@in.tum.de>
2017-09-06 21:56 GMT+02:00 Makarius <makarius@sketis.net>:
On 06/09/17 18:44, Lars Hupel wrote:
I just loaded Monad_Syntax in Isabelle2017-RC1 and observed that it
pulls
in many dependencies. In particular, it transitively depends
on Old_Datatype. This is not a bug, but very surprising behavior to
me: I
would expect only additional syntactic sugar from a theory that calls
itself _Syntax and not a huge set of Old_ functionality.That is partly my fault.
changeset: 66260:466d8e7ed170
user: Lars Hupel <lars.hupel@mytum.de>
date: Mon Jul 10 23:21:54 2017 +0200
summary: FSet is monadicMonad_Syntax sets up sugar for finite sets, which pulls in "Countable",
which provides a tactic that works on "Old_Datatype".Is there a genuine problem behind it? Otherwise I would say we leave it
like that for the release.
If we keep FSet in Monad_Syntax, then everybody who uses Monad_Syntax also
gets all the lemmata, tactics, simpset (if it changes anything) from FSet,
Countable, and Old_Datatype into its namespace. This may change the
behavior of sledgehammer and other automated tools. This may make certain
things harder to reproduce. I don't know of any particular issue, but I may
think of a future issue like "sledgehammer and auto can only solve a
subgoal if I include Monad_Syntax. But I don't have any monad syntax in my
thy." As I said, my feeling about a theory which is named *_Syntax is that
it should not provide more than syntactic sugar.
My personal feeling is that FSet should get removed from Monad_Syntax.
Currently, we should be able to do this without breaking any dependencies
for users of the stable release.
In Isabelle2016-1 we have
theory Monad_Syntax
imports Main "~~/src/Tools/Adhoc_Overloading"
In Isabelle2017-RC1 we have
theory Monad_Syntax
imports FSet "~~/src/Tools/Adhoc_Overloading"
Maybe one could add the monad syntax to FSet. But then FSet would depend on
Monad_Syntax, ... a chicken-or-egg dilemma.
Maybe we we need a theory similar to
theory FSet_Monad_Syntax
imports FSet Monad_Syntax
begin
adhoc_overloading FSet.fbind
end
This would also be a really helpful example. It took me more than one hour
to understand how I can get the monad syntax to work with my custom bind
function for my custom datatype.
But maybe I'm overfitting stuff here according to my personal preferences.
But I guess once we have FSet as dependency in Monad_Syntax (which is
currently NOT the case for Isabelle2016-1), we can nevever go back (without
breaking anything).
Cheers,
Cornelius
Email Gateway (Aug 22 2022 at 16:03):From: Tobias Nipkow <nipkow@in.tum.de>
I agree with Cornelius. If possible the dependency on FSet should be removed
before the release. If not, I assume Lars will remove it afterwards, which may
then create new complications for the release after this one.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 16:03):From: Lars Hupel <hupel@in.tum.de>
I have no strong opinion. I also don't think anybody uses this yet, so
Makarius, please back out 466d8e7ed170 from the release fork.
Cheers
Lars
Email Gateway (Aug 22 2022 at 16:03):From: Makarius <makarius@sketis.net>
I am about to do this, but note that the release fork did not happen
yet. (I am still waiting for some updates on Nunchaku.)
Makarius
Last updated: Apr 16 2024 at 20:15 UTC