Zulip Chat Archive

Stream: new members

Topic: CNL-CIC

Lucas Teixeira (Oct 27 2021 at 10:54):

Does anyone have any experience using CNL-CIC??

https://github.com/formalabstracts/CNL-CIC

I've gotten as far as cloning the repo, and I've browsed through the documentation, but I still have yet to:

  1. See any examples of content written in CNL-CIC
  2. Write scripts in CNL-CIC and compile them to LEAN

Mario Carneiro (Oct 27 2021 at 10:57):

There are examples in the planet-math folder, e.g. https://github.com/formalabstracts/CNL-CIC/blob/master/sample-texts/planet-math-11/11P32-LevysConjecture.tex

Mario Carneiro (Oct 27 2021 at 10:59):

Keep in mind that the project is essentially abandoned at this point, and AFAIK there was never a really polished version produced, so making it work may be an uphill battle

Mario Carneiro (Oct 27 2021 at 10:59):

There is a longer example about sylow's theorems here: https://github.com/formalabstracts/CNL-CIC/blob/master/TeX2CNL/tex/sample_sylow.tex

Lucas Teixeira (Oct 27 2021 at 11:15):

Word, thanks!

This is more of a LaTeX question... but would you happen to know how I can get a hold of the cnl package??

Johan Commelin (Oct 27 2021 at 11:16):

Is it this thing? https://github.com/formalabstracts/CNL-CIC/tree/master/TeX2CNL/tex

Lucas Teixeira (Oct 27 2021 at 11:19):

I'm not sure, but I don't think so. I'm a big LaTeX noob

When I run the examples through TeXworks I get the error ! LaTeX Error: File 'cnl.sty' not found. which I'm assuming comes from \usepackage{cnl}

Johan Commelin (Oct 27 2021 at 11:22):

Tip: You can write `` Look, here's a backtick ` It works! `` .

Johan Commelin (Oct 27 2021 at 11:22):

Add more backticks if needed.

Lucas Teixeira (Oct 27 2021 at 11:42):

Actually looking further into it I think you are right. I just have to look into how to get this to work with my setup

Lucas Teixeira (Oct 28 2021 at 01:12):

I figured it out. So the file which usepackage{cnl} is refering to is actually this one:

https://github.com/formalabstracts/CNL-CIC/blob/master/TeX2CNL/package/cnl.sty

We're getting the above error because we actually to import packages which are outside of the main directory, we need to plug in the full path name. After changing usepackage{cnl} to \usepackage{/home/user/moss/CNL-CIC/TeX2CNL/package/cnl}** it works

**Mind you, the /home/user/moss/ is specific to my particular machine

Last updated: Dec 20 2023 at 11:08 UTC