bugBRILLANT - Bugs: bug #22075, Wrong LaTeX macro for \notin B...

Show feedback again

You are not allowed to post comments on this tracker with your current authentification level.

bug #22075: Wrong LaTeX macro for \notin B symbol

Submitted by:  Piotr Trojanek <ptroja>
Submitted on:  Fri 23 May 2014 11:06:55 AM UTC  
Category: NoneModule: Docs
Priority: 5 - NormalSeverity: 2 - Minor
Status: ConfirmedPrivacy: Public
Assigned to: NoneOpen/Closed: Open

Mon 01 Sep 2014 04:16:24 PM UTC, SVN revision 1498:

Fix bug #22075

(Browse SVN revision 1498)

Samuel Colin <scolin>
Project Administrator
Tue 03 Jun 2014 08:51:19 AM UTC, comment #2:

I took a look, the bug is confirmed.
The correct ASCII syntax for \notin is /: (as is described in the B reference manual or as is seen in the examples of bbench/)

As for duplicates, there are indeed three files:
./bcaml/toolchain/btyper2/lib/doc/B2.sty : probably the most recent
./latex/B2/B2.sty : the oldest

Fixing this would entail:
- Replacing :/ by /:
- Integrate the event-B keywords of docs/brillant-bcaml/B2.sty into bcaml/toolchain/btyper2/lib/doc/B2.sty (saw that with a quick diff, but there might be a few more macros to integrate)
- Copy bcaml/toolchain/btyper2/lib/doc/B2.sty as latex/B2/B2.sty
- Symlink the other files to latex/B2/B2.sty

Samuel Colin <scolin>
Project Administrator
Tue 27 May 2014 08:54:28 AM UTC, comment #1:

Hello Piotr

Sorry I don't understand clearly your bug report.

find . -name B2.sty | xargs grep notin

gives me


with the correct assignement :/ in the three cases...

B2.sty was designed by Samuel to be used in the context of the "listing" LaTeX package. The associated test.tex file is compiled correctly (right typesetting of notin...)

Right. There should be only one B2.styn the one located in latex/B2...

PS : do you want to be added in the devs group for BRILLANT so that you can commit your ideas/corrections ...? (just ask)

Georges Mariano <gmariano>
Project Administrator
Fri 23 May 2014 11:06:55 AM UTC, original submission:

All three B2.sty files in the repository define the \notin symbol as ":/" instead of "/:".

First, I am not sure why there are three B2.sty files instead of one. Second, I am not sure if there is some hidden reason for using the current notation. Anyway, it is trivial to fix.

Piotr Trojanek <ptroja>


No files currently attached


Depends on the following items: None found

Items that depend on this one: None found


Carbon-Copy List
  • -unavailable- added by scolin (Posted a comment)
  • -unavailable- added by gmariano (Posted a comment)
  • -unavailable- added by ptroja (Submitted the item)

    Do you think this task is very important?
    If so, you can click here to add your encouragement to it.
    This task has 0 encouragements so far.

    Only logged-in users can vote.


    Error: not logged in



    Follow 4 latest changes.

    Date Changed By Updated Field Previous Value => Replaced By
    Tue 03 Jun 2014 08:51:19 AM UTCscolinModuleNone=>Docs
      SummaryWrong LaTeX macro for \\notin B symbol=>Wrong LaTeX macro for \notin B symbol
    Tue 27 May 2014 08:54:28 AM UTCgmarianoSummaryWrong LaTeX macro for \\notin B symbol=>Wrong LaTeX macro for \notin B symbol
    Show feedback again

    Back to the top

    Powered by Savane 3.1-cleanup