You can subscribe to this list here.
2009 
_{Jan}
(10) 
_{Feb}
(57) 
_{Mar}
(16) 
_{Apr}
(15) 
_{May}
(31) 
_{Jun}
(17) 
_{Jul}
(10) 
_{Aug}
(18) 
_{Sep}
(20) 
_{Oct}
(31) 
_{Nov}
(6) 
_{Dec}
(7) 

2010 
_{Jan}
(21) 
_{Feb}
(40) 
_{Mar}
(35) 
_{Apr}
(14) 
_{May}
(21) 
_{Jun}
(6) 
_{Jul}
(33) 
_{Aug}
(97) 
_{Sep}
(55) 
_{Oct}
(37) 
_{Nov}
(35) 
_{Dec}
(23) 
2011 
_{Jan}
(9) 
_{Feb}
(9) 
_{Mar}
(57) 
_{Apr}
(21) 
_{May}
(4) 
_{Jun}
(6) 
_{Jul}
(12) 
_{Aug}
(13) 
_{Sep}
(18) 
_{Oct}
(9) 
_{Nov}
(11) 
_{Dec}
(3) 
2012 
_{Jan}
(45) 
_{Feb}
(18) 
_{Mar}
(18) 
_{Apr}
(14) 
_{May}
(11) 
_{Jun}
(14) 
_{Jul}
(3) 
_{Aug}
(6) 
_{Sep}
(2) 
_{Oct}
(16) 
_{Nov}
(31) 
_{Dec}
(10) 
2013 
_{Jan}
(29) 
_{Feb}
(7) 
_{Mar}
(21) 
_{Apr}
(52) 
_{May}
(32) 
_{Jun}
(8) 
_{Jul}
(9) 
_{Aug}
(9) 
_{Sep}
(7) 
_{Oct}
(22) 
_{Nov}
(12) 
_{Dec}

2014 
_{Jan}
(36) 
_{Feb}
(11) 
_{Mar}
(11) 
_{Apr}
(18) 
_{May}
(8) 
_{Jun}
(19) 
_{Jul}
(15) 
_{Aug}
(22) 
_{Sep}
(11) 
_{Oct}
(8) 
_{Nov}
(4) 
_{Dec}
(14) 
2015 
_{Jan}
(2) 
_{Feb}
(4) 
_{Mar}
(10) 
_{Apr}
(7) 
_{May}
(11) 
_{Jun}
(17) 
_{Jul}
(5) 
_{Aug}

_{Sep}

_{Oct}

_{Nov}

_{Dec}

S  M  T  W  T  F  S 




1

2

3

4

5

6
(2) 
7
(2) 
8
(3) 
9
(4) 
10
(1) 
11

12

13
(1) 
14
(7) 
15

16
(1) 
17
(1) 
18

19

20

21

22

23

24
(1) 
25

26

27

28

29

30

31


From: Mathieu Clabaut <mathieu.clabaut@sy...>  20101224 13:15:03

Hello, I've got the following goal : ran(({max(dom(buffer(d)))} ⩤ buffer(d))∪{max(dom(buffer(d))) ↦ (x ↦ request ↦ s ↦ d)}) = X whene none of the symbols except the equal sign are activated (i.e. clickable). I then would have expect that at least ∪ is activated and allowed me to apply DISTRI_RAN_BUNION. But it is not the case. Is this an expected behaviour ? Using *ae* on both sides and the doing an *ah* on ran(ae ∪ ae0) = ran(ae) ∪ ran(ae0) works but is very cumbersome ! Best regards and Happy Christmas to all, Mathieu   Mathieu Clabaut Tél. : (+33)(0)4 42 90 65 51 SYSTEREL  Standard / Fax : (+33)(0)4 42 90 41 20 / 29 site : http://www.systerel.fr  
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20101217 08:26:18

BEGIN PGP SIGNED MESSAGE Hash: SHA1 Dear Benoit, > the following rules have been added on the wiki: > > SIMP_DOMRES_DOMSUB_ID > SIMP_RANRES_DOMSUB_ID > SIMP_DOMSUB_DOMSUB_ID > SIMP_RANSUB_DOMSUB_ID > > SIMP_RANRES_ID > SIMP_RANSUB_ID > > SIMP_MULTI_DOMSUB_RAN > SIMP_MULTI_RANSUB_DOM They seem all to be sound. Thanks for maintaining the rules.  Matthias BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFNCx6bczhznXSdWggRAtO8AJ9Q+bSREM1/+s0wr2jrJw5qtc10JgCgp0FY rZWSEH438joyhoTnivO4rGQ= =wd7R END PGP SIGNATURE 
From: Benoît Lucet <benoit.lucet@sy...>  20101216 14:40:06

Dear All, the following rules have been changed on the wiki : SIMP_DOMRES_ID renamed in SIMP_DOMRES_DOMRES_ID SIMP_RANRES_ID renamed in SIMP_RANRES_DOMRES_ID SIMP_DOMSUB_ID renamed in SIMP_DOMSUB_DOMRES_ID SIMP_RANSUB_ID renamed in SIMP_RANSUB_DOMRES_ID the following rules have been added on the wiki: SIMP_DOMRES_DOMSUB_ID SIMP_RANRES_DOMSUB_ID SIMP_DOMSUB_DOMSUB_ID SIMP_RANSUB_DOMSUB_ID SIMP_RANRES_ID SIMP_RANSUB_ID SIMP_MULTI_DOMSUB_RAN SIMP_MULTI_RANSUB_DOM Could you please review these new rules ? Cheers, Benoît 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20101214 13:09:13

BEGIN PGP SIGNED MESSAGE Hash: SHA1 Dear Laurent, I was expecting to be able to click on the membership operator, and forgot to try simplification rewrites. So I withdraw my request. If I encounter any problems, I let you know.  Matthias Laurent Voisin schrieb: > Dear Matthias, > > Le 14 déc. 2010 à 11:45, Matthias Schmalz a écrit : > >> since you are working on the rules, could you please consider >> implementing betareduction rules, i.e., rules that rewrite >> >> $x : {y1, ..., yn. $phi(y1, ..., yn)  $f(y1, ..., yn)} >> to >> # y1, ..., yn. $phi(y1, ..., yn) & $x = $f(y1, ..., yn) >> >> and >> >> $x : {y$phi(y)} >> to >> $phi($x)? > > To my knowledge, both of these rules are implemented in the AutoRewriter (tactic Simplification rewrites). > > Are there cases where this does not apply? Or do you need something special? > > Cheers, > Laurent. > BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFNB2xwczhznXSdWggRAhg+AKCbXO6cfmNF2bD/URhptb7zOmlnKQCgpLbs d1Kmh0PouJte+ev7UQpBgGk= =Dvki END PGP SIGNATURE 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20101214 13:07:04

BEGIN PGP SIGNED MESSAGE Hash: SHA1 Dear Laurent, the rules seem to be sound.  Matthias Laurent Voisin schrieb: > Dear Matthias, > > Le 14 déc. 2010 à 11:40, Matthias Schmalz a écrit : > >> I think the /bigcap is a binder; so the rule would be syntactically >> incorrect. Did I miss something? > > No, you're right, there was a typo in the LaTeX source ("\Inter" instead of "\inter"). > > I took this opportunity to fix this rule and add a new one for generalised intersection. Now, the two rules to review are > > FIN_KINTER_R > FIN_QINTER_R > > Do you agree with them ? > > Laurent. > >> Nicolas Beauger schrieb: >>> Dear All, >>> >>> A new inference rule has been added to the wiki: >>> >>> FIN_QINTER_R in http://wiki.eventb.org/index.php/Inference_Rules >>> >>> Can you please check that it is sound ? >>> >>> Cheers, >>> Nicolas >>> >>>  >>>  >>> Nicolas BEAUGER Tél. : (+33)(0)4 42 90 65 66 >>> Ingénieur Logiciel >>> >>> SYSTEREL >>>  >>> Standard / Fax : (+33)(0)4 42 90 41 20 / 29 site : http://www.systerel.fr >>>  >>> >> BEGIN PGP SIGNATURE >> Version: GnuPG v1.4.6 (GNU/Linux) >> Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org >> >> iD8DBQFNB0mNczhznXSdWggRAq9vAJ40K9HUUB0buw/8FKotiqDv682TQACeMIA4 >> zaMXd6elZXyx78/w2tYKMZI= >> =jTfr >> END PGP SIGNATURE >> >>  >> Lotusphere 2011 >> Register now for Lotusphere 2011 and learn how >> to connect the dots, take your collaborative environment >> to the next level, and enter the era of Social Business. >> http://p.sf.net/sfu/lotusphered2d >> _______________________________________________ >> Rodinbsharpuser mailing list >> Rodinbsharpuser@... >> https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser > BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFNB2vvczhznXSdWggRAmFuAJwKbQY1KmcjB1JGFTeLi6WbvCVx4wCeL0Rd aNdES7rBqEnuZ+PoBM/uxyw= =r0vZ END PGP SIGNATURE 
From: Laurent Voisin <laurent.voisin@sy...>  20101214 13:01:46

Dear Matthias, Le 14 déc. 2010 à 11:45, Matthias Schmalz a écrit : > since you are working on the rules, could you please consider > implementing betareduction rules, i.e., rules that rewrite > > $x : {y1, ..., yn. $phi(y1, ..., yn)  $f(y1, ..., yn)} > to > # y1, ..., yn. $phi(y1, ..., yn) & $x = $f(y1, ..., yn) > > and > > $x : {y$phi(y)} > to > $phi($x)? To my knowledge, both of these rules are implemented in the AutoRewriter (tactic Simplification rewrites). Are there cases where this does not apply? Or do you need something special? Cheers, Laurent. 
From: Laurent Voisin <laurent.voisin@sy...>  20101214 12:59:45

Dear Matthias, Le 14 déc. 2010 à 11:40, Matthias Schmalz a écrit : > I think the /bigcap is a binder; so the rule would be syntactically > incorrect. Did I miss something? No, you're right, there was a typo in the LaTeX source ("\Inter" instead of "\inter"). I took this opportunity to fix this rule and add a new one for generalised intersection. Now, the two rules to review are FIN_KINTER_R FIN_QINTER_R Do you agree with them ? Laurent. > Nicolas Beauger schrieb: >> Dear All, >> >> A new inference rule has been added to the wiki: >> >> FIN_QINTER_R in http://wiki.eventb.org/index.php/Inference_Rules >> >> Can you please check that it is sound ? >> >> Cheers, >> Nicolas >> >>  >>  >> Nicolas BEAUGER Tél. : (+33)(0)4 42 90 65 66 >> Ingénieur Logiciel >> >> SYSTEREL >>  >> Standard / Fax : (+33)(0)4 42 90 41 20 / 29 site : http://www.systerel.fr >>  >> > BEGIN PGP SIGNATURE > Version: GnuPG v1.4.6 (GNU/Linux) > Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org > > iD8DBQFNB0mNczhznXSdWggRAq9vAJ40K9HUUB0buw/8FKotiqDv682TQACeMIA4 > zaMXd6elZXyx78/w2tYKMZI= > =jTfr > END PGP SIGNATURE > >  > Lotusphere 2011 > Register now for Lotusphere 2011 and learn how > to connect the dots, take your collaborative environment > to the next level, and enter the era of Social Business. > http://p.sf.net/sfu/lotusphered2d > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20101214 11:15:56

BEGIN PGP SIGNED MESSAGE Hash: SHA1 Dear Laurent, ... > Do you agree with my argument above ? Yes. > Do you have any suggestion for rewording the sidecondition so that > it is easier to understand / check ? First off, I would replace {x. P  E > F} by {x1, ..., xn. P  E > F}. My proposal for the sideconditions of both SIMP_CARD_LAMBDA and SIMP_FINITE_LAMBDA: 1. E is \emph{admissible}, where the set of admissible expressions is the smallest set satisfying the following conditions:   x1, ..., xn are admissible.   If none of x1, ..., xn is free in E, then E is admissible.   If E1 and E2 are admissible, then so is E1 > E2. 2. If xi is free in F, then xi is free in E, 1 <= i <= n. These sideconditions ensure that {x1, ..., xn. P  E > F} : TE +> TF, where TE is the type of E and TF the type of F.  Matthias BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFNB1HjczhznXSdWggRAkKuAJ0UeWbgkScsTYvEWHIoz/5N+v++VgCgjFdL SKxjq84LJLNIoQ1YT1DvhJI= =bHVo END PGP SIGNATURE 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20101214 10:46:04

BEGIN PGP SIGNED MESSAGE Hash: SHA1 Dear Laurent, Nicolas, since you are working on the rules, could you please consider implementing betareduction rules, i.e., rules that rewrite $x : {y1, ..., yn. $phi(y1, ..., yn)  $f(y1, ..., yn)} to # y1, ..., yn. $phi(y1, ..., yn) & $x = $f(y1, ..., yn) and $x : {y$phi(y)} to $phi($x)? Cheers, Matthias P.s.: I use the notation of my report. If you restate the rules with substitutions, you will need some sideconditions. BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFNB0rkczhznXSdWggRAlzzAJ0Z/Lnl0Pc+DerLtkFGmrerw6m1iACdHISu f23sbhBGfuiz0wMyAFDpncg= =Olyd END PGP SIGNATURE 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20101214 10:40:23

BEGIN PGP SIGNED MESSAGE Hash: SHA1 Nicolas, I think the /bigcap is a binder; so the rule would be syntactically incorrect. Did I miss something?  Matthias Nicolas Beauger schrieb: > Dear All, > > A new inference rule has been added to the wiki: > > FIN_QINTER_R in http://wiki.eventb.org/index.php/Inference_Rules > > Can you please check that it is sound ? > > Cheers, > Nicolas > >  >  > Nicolas BEAUGER Tél. : (+33)(0)4 42 90 65 66 > Ingénieur Logiciel > > SYSTEREL >  > Standard / Fax : (+33)(0)4 42 90 41 20 / 29 site : http://www.systerel.fr >  > BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFNB0mNczhznXSdWggRAq9vAJ40K9HUUB0buw/8FKotiqDv682TQACeMIA4 zaMXd6elZXyx78/w2tYKMZI= =jTfr END PGP SIGNATURE 
From: Nicolas Beauger <nicolas.beauger@sy...>  20101213 17:09:41

Dear All, A new inference rule has been added to the wiki: FIN_QINTER_R in http://wiki.eventb.org/index.php/Inference_Rules Can you please check that it is sound ? Cheers, Nicolas   Nicolas BEAUGER Tél. : (+33)(0)4 42 90 65 66 Ingénieur Logiciel SYSTEREL  Standard / Fax : (+33)(0)4 42 90 41 20 / 29 site : http://www.systerel.fr  
From: Laurent Voisin <laurent.voisin@sy...>  20101210 13:25:17

Dear Matthias, thank you for your feedback. Le 9 déc. 2010 à 09:26, Matthias Schmalz a écrit : >> SIMP_FINITE_LAMBDA >> SIMP_FINITE_LAMBDA > > Why the duplication? I meant SIMP_CARD_LAMBDA, sorry for the confusion. > Why is the rule in the category of "set rewrite rules"? Well, I think it is mainly historical. All rules about FINITE have been put in this page. > The sidecondition is unclear: "... expressions that are not bound by > the comprehension set". A binder does not bind expressions, a binder > binds variables. The purpose of the sidecondition is to ensure that the comprehension set is a function. When it is the case, we can assume that the ``size'' of the comprehension set is the same as that of its domain. More formally, there exists a bijection between the function and its domain (which is the first projection). The rewriting proposed by the rules for both finiteness and cardinality follows from this property. Coming back to the comprehension set being a function, we want to ensure it based on a syntactical property. What we need is that given a set {x . P  E>F}, for every pairs of maplets E1 > F1 and E2 > F2 belonging to the set, we have F1 = F2 whenever E1 = E2. We then consider E and F as functions of the variables x that are bound by the comprehension set. In the sequel, I will use the shorthand "locally bound" to denote variables that are bound by the comprehension set. The criteria (which is only a sufficient condition) is that : 1. E looks like a tree constructed with maplet operators, all the leafs of which are either locally bound variables alone or expressions where no locally bound variable occurs. 2. All locally bound variables that occur in F also occur in E. The first condition ensures that E is an injective function with respect to the locally bound variables (because maplets are injective). The second condition allows to ensure that E contains all the locally bound variable used in F. > Does the sidecondition rule out {x. true  x*0 > x}? Yes, because the lefthand side of the pair is not injective in "x". Do you agree with my argument above ? Do you have any suggestion for rewording the sidecondition so that it is easier to understand / check ? Laurent. 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20101209 08:42:04

BEGIN PGP SIGNED MESSAGE Hash: SHA1 Dear Benoît, the rules seem all to be sound.  Matthias Benoît Lucet schrieb: > Dear All, > > the following rule has been changed on the wiki : > > SIMP_CARD_ID has been renamed in SIMP_CARD_ID_DOMRES > > the following rules were added on the wiki : > > SIMP_FINITE_ID_DOMRES > > SIMP_FINITE_PRJ1 > SIMP_FINITE_PRJ2 > SIMP_FINITE_PRJ1_DOMRES > SIMP_FINITE_PRJ2_DOMRES > > SIMP_CARD_ID > > SIMP_CARD_PRJ1 > SIMP_CARD_PRJ2 > SIMP_CARD_PRJ1_DOMRES > SIMP_CARD_PRJ2_DOMRES > > Could you please review these new rules ? > > Cheers, > Benoît > >  > What happens now with your Lotus Notes apps  do you make another costly > upgrade, or settle for being marooned without product support? Time to move > off Lotus Notes and onto the cloud with Force.com, apps are easier to build, > use, and manage than apps on traditional platforms. Sign up for the Lotus > Notes Migration Kit to learn more. http://p.sf.net/sfu/salesforced2d > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFNAJZUczhznXSdWggRArElAJ9O4rht6sVvgOVlohDMrOpo6d6RXACfSXZY S8LbB1QyPKbP7jdShZ1zFTI= =Z2mU END PGP SIGNATURE 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20101209 08:26:50

BEGIN PGP SIGNED MESSAGE Hash: SHA1 Dear Laurent, > SIMP_DOM_LAMBDA > SIMP_RAN_LAMBDA > SIMP_TYPE_OVERL_CPROD Sound. > SIMP_FINITE_LAMBDA > SIMP_FINITE_LAMBDA Why the duplication? Why is the rule in the category of "set rewrite rules"? The sidecondition is unclear: "... expressions that are not bound by the comprehension set". A binder does not bind expressions, a binder binds variables. Does the sidecondition rule out {x. true  x*0 > x}? The planned implementation may be sound, but it does not have to be.  Matthias BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFNAJK9czhznXSdWggRAj53AJ45kmbcz6U2YBUe2HcbSLmzIwYrqwCgolqX MJD/l897Q57v9oIER32Px0k= =5lFq END PGP SIGNATURE 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20101209 08:14:29

BEGIN PGP SIGNED MESSAGE Hash: SHA1 Dear Samah, EventB does not support overloading. Hence you will need two constants idle, e.g., idle1 (of type set1) and idle2 (of type set2).  Matthias Samah Hassan schrieb: > Dear all, > > I am trying to write a model for a motor and a shaft, which both had a > state *idle, *it seems that RODIN does not accept that a constant > belongs to two different sets > it gives the following errors: > > Type unKnown > Types set1 and set2 does not match > > below is the context file > > * * > > *context* > > ctx1 > > *constants* > > *clockwise* > > *counterclockwise* > > *idle* > > *up* > > ** > > *down*** > > * * > > *sets* > > *set2* > > *set1* > > ** > > ***axioms* > > @axm1 *set2* = {**clockwise , **counterclockwise , **idle **} > > @axm2 *clockwise*≠ * *counterclockwise ** > > **@axm3 *clockwise* ≠ *idle* > > **@axm4 * *counterclockwise ** ≠ *idle* > > @axm5 *set1* = {*up*, *down*, *idle*} > > @axm6 *up* ≠ *down* > > @axm7 *up* ≠ *idle* > > @axm8 *down* ≠ *idle* > > > > *end* > > ** > > Any suggestions on how to resolve that error and keep the model as it is? > > > > Thanks, > > Samah > > > > > > BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFNAI/XczhznXSdWggRAq96AKCrEvX/2VYhmP8qALrmOo0nG45dIgCcDFwX 6G7UMOgqbTrQTzkBHjLEsbo= =AE7P END PGP SIGNATURE 
From: Samah Hassan <samah_3@ya...>  20101209 06:28:24

Dear all, I am trying to write a model for a motor and a shaft, which both had a state idle, it seems that RODIN does not accept that a constant belongs to two different sets it gives the following errors: Type unKnown Types set1 and set2 does not match below is the context file contextctx1constantsclockwisecounterclockwiseup setsset2 axioms@...≠ idle @axm4 counterclockwise ≠ idle@...= {up, down, idle}@axm6 up≠ down@... up≠ idle@... down≠ idle Any suggestions on how to resolve that error and keep the model as it is? Thanks, Samah end@...= {clockwise , counterclockwise , idle }@axm2 clockwise≠ counterclockwise set1 downidle 
From: Colin Snook <cfs@ec...>  20101208 15:39:43

Hi Louis, We recommend you install the Teamwork plugin which is designed to assist with sharing into model repositories. This configures the SVN ignore settings automatically for you and then provides a synchronised copy of your machines that can be committed retrieved and compared with a copy in a repository. see http://wiki.eventb.org/index.php/Teambased_development Regards Colin On 7 Dec 2010, at 20:11, Louis Bernath wrote: > Hello > > We are trying to share a Rodin project in a SVN repository. After a svn > update from the repository, Rodin claims 100+ errors, like "component > ctx does not have a configuration" in ctx.bcc_tmp. > > Has anybody experience using SVN or any other source repository? Any > hints on excluding some filetypes from synchronization? > > Any help would be greatly appreciated. > > Kind regards > Louis > >  > What happens now with your Lotus Notes apps  do you make another costly > upgrade, or settle for being marooned without product support? Time to move > off Lotus Notes and onto the cloud with Force.com, apps are easier to build, > use, and manage than apps on traditional platforms. Sign up for the Lotus > Notes Migration Kit to learn more. http://p.sf.net/sfu/salesforced2d > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser 
From: Laurent Voisin <laurent.voisin@sy...>  20101208 15:25:16

Dear Louis, Le 7 déc. 2010 à 21:11, Louis Bernath a écrit : > We are trying to share a Rodin project in a SVN repository. After a svn > update from the repository, Rodin claims 100+ errors, like "component > ctx does not have a configuration" in ctx.bcc_tmp. > > Has anybody experience using SVN or any other source repository? Any > hints on excluding some filetypes from synchronization? > > Any help would be greatly appreciated. The .bcc_tmp and .bpo_tmp are temporary files and shall not be version controlled. You can instruct SVN to ignore them by using the svnignore property on the project directory. Cheers, Laurent. 
From: Benoît Lucet <benoit.lucet@sy...>  20101208 14:53:43

Dear All, the following rule has been changed on the wiki : SIMP_CARD_ID has been renamed in SIMP_CARD_ID_DOMRES the following rules were added on the wiki : SIMP_FINITE_ID_DOMRES SIMP_FINITE_PRJ1 SIMP_FINITE_PRJ2 SIMP_FINITE_PRJ1_DOMRES SIMP_FINITE_PRJ2_DOMRES SIMP_CARD_ID SIMP_CARD_PRJ1 SIMP_CARD_PRJ2 SIMP_CARD_PRJ1_DOMRES SIMP_CARD_PRJ2_DOMRES Could you please review these new rules ? Cheers, Benoît 
From: Louis Bernath <bernl1@bf...>  20101207 20:34:41

Hello We are trying to share a Rodin project in a SVN repository. After a svn update from the repository, Rodin claims 100+ errors, like "component ctx does not have a configuration" in ctx.bcc_tmp. Has anybody experience using SVN or any other source repository? Any hints on excluding some filetypes from synchronization? Any help would be greatly appreciated. Kind regards Louis 
From: Laurent Voisin <laurent.voisin@sy...>  20101207 11:37:19

Dear All, here is another list of rewrite rules that have been changed in the wiki. They have been changed to enlarge the cases where they are applicable, thus improving the prover performance. SIMP_DOM_LAMBDA SIMP_RAN_LAMBDA SIMP_FINITE_LAMBDA SIMP_FINITE_LAMBDA SIMP_TYPE_OVERL_CPROD As concerns rules SIMP_FINITE_LAMBDA and SIMP_FINITE_LAMBDA, the argument is that the cardinality is not changed when one goes from a function to its domain. To detect that a comprehension set is a function, we rely on the syntactical injectivity of the lefthand side of the maplet, which is ensured by patternmatching. Any feedback on these new versions of the rules is welcome. Cheers, Laurent. 
From: Matthias Schmalz <Matthias.S<chmalz@in...>  20101206 14:15:54

BEGIN PGP SIGNED MESSAGE Hash: SHA1 Laurent, they seem to be sound.  Matthias Laurent Voisin schrieb: > Dear All, > > the following rules have been changed on the wiki : > > SIMP_TYPE_CONVERSE has been generalised to SIMP_CONVERSE_CPROD > SIMP_TYPE_DPROD has been generalised to SIMP_DPROD_CPROD > SIMP_TYPE_PPROD has been generalised to SIMP_PPROD_CPROD > > The original rules were unnecessarily restricted and are subsumed by the new ones. > > SIMP_TYPE_OVERL_CPROD has been removed > > This rule was wrong when the righthand side was empty. > > SIMP_IN_FUNIMAGE > SIMP_IN_FUNIMAGE_CONVERSE_L > SIMP_IN_FUNIMAGE_CONVERSE_R > SIMP_FINITE_UNION > SIMP_FINITE_QUNION > > These are new rules added following to a suggestion of JeanRaymond Abrial. > > Could you please review these new rules that will be part of the next Rodin release ? > > Cheers, > Laurent. >  > What happens now with your Lotus Notes apps  do you make another costly > upgrade, or settle for being marooned without product support? Time to move > off Lotus Notes and onto the cloud with Force.com, apps are easier to build, > use, and manage than apps on traditional platforms. Sign up for the Lotus > Notes Migration Kit to learn more. http://p.sf.net/sfu/salesforced2d > _______________________________________________ > Rodinbsharpuser mailing list > Rodinbsharpuser@... > https://lists.sourceforge.net/lists/listinfo/rodinbsharpuser BEGIN PGP SIGNATURE Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla  http://enigmail.mozdev.org iD8DBQFM/PASczhznXSdWggRAsGHAJ4qo3J8GJhusAhReAvhqFkIpr0b9wCfapUe BAD5EfblN4ufzhX1hlcW4P8= =ICDx END PGP SIGNATURE 
From: Laurent Voisin <laurent.voisin@sy...>  20101206 13:40:16

Dear All, the following rules have been changed on the wiki : SIMP_TYPE_CONVERSE has been generalised to SIMP_CONVERSE_CPROD SIMP_TYPE_DPROD has been generalised to SIMP_DPROD_CPROD SIMP_TYPE_PPROD has been generalised to SIMP_PPROD_CPROD The original rules were unnecessarily restricted and are subsumed by the new ones. SIMP_TYPE_OVERL_CPROD has been removed This rule was wrong when the righthand side was empty. SIMP_IN_FUNIMAGE SIMP_IN_FUNIMAGE_CONVERSE_L SIMP_IN_FUNIMAGE_CONVERSE_R SIMP_FINITE_UNION SIMP_FINITE_QUNION These are new rules added following to a suggestion of JeanRaymond Abrial. Could you please review these new rules that will be part of the next Rodin release ? Cheers, Laurent. 