Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Repo info
Activity
  • Sep 05 2021 05:38

    siddhartha-gadgil on master

    removed project/.bloop (compare)

  • Sep 05 2021 01:45

    siddhartha-gadgil on master

    removed bsp (compare)

  • Jul 17 2021 06:10

    siddhartha-gadgil on master

    removed pprints from SAT solver (compare)

  • Jul 05 2021 12:24

    siddhartha-gadgil on master

    tweaks to text queens (compare)

  • Jul 05 2021 12:09

    siddhartha-gadgil on master

    NQueens prints text (compare)

  • May 15 2021 11:49

    siddhartha-gadgil on master

    queens html picture SAT model/proof html output (compare)

  • May 06 2021 06:25

    siddhartha-gadgil on master

    separating indexing from back t… (compare)

  • May 03 2021 10:31

    siddhartha-gadgil on master

    helper (compare)

  • May 01 2021 04:56

    siddhartha-gadgil on master

    cleaner solutions, common trait (compare)

  • Apr 28 2021 13:59

    siddhartha-gadgil on master

    reviving fol refactoring fol tweaks; need formal variables and 10 more (compare)

  • Apr 28 2021 13:58

    siddhartha-gadgil on fol

    more bugs fixed, NQueens works (compare)

  • Apr 28 2021 13:13

    siddhartha-gadgil on fol

    more bugs corrected, some cases… (compare)

  • Apr 28 2021 12:09

    siddhartha-gadgil on fol

    some debugging (compare)

  • Apr 28 2021 10:04

    siddhartha-gadgil on fol

    steps for solver with proof and… (compare)

  • Apr 27 2021 13:59

    siddhartha-gadgil on fol

    eight queens solved (compare)

  • Apr 27 2021 12:00

    siddhartha-gadgil on fol

    map as output (compare)

  • Apr 27 2021 11:02

    siddhartha-gadgil on fol

    correction, purging tautologies (compare)

  • Apr 27 2021 10:06

    siddhartha-gadgil on fol

    dpll correction, clean up (compare)

  • Apr 27 2021 08:41

    siddhartha-gadgil on fol

    DPLL code, untested (compare)

  • Apr 27 2021 05:39

    siddhartha-gadgil on fol

    allowing formula variables (compare)

babu-akhil
@babu-akhil
What does +U mean in this definition trait Func[W <: Term with Subs[W], +U <: Term with Subs[U]]
Piotr Paradziński
@lemastero

I'd like to play around with ProvingGround - I am Scala programmer so I thought I will try to address some issue marked as newbie-friendly like this: siddhartha-gadgil/ProvingGround#166
is it a good idea.

Maybe going through this course first: https://stepik.org/course/49181/promo would be better? I did some reading/watching around HoTT before (A. Thorsten lectures etc) but HoTT book is still on my reading list (I failed a few times already) :)

Siddhartha Gadgil
@siddhartha-gadgil
@lemastero sorry I didn't check this chat for a long time.
You are of course most welcome to play around.
Those issues are important, and good to approach as there are tests to avoid breaking anything.
They are a bit intricate as they need a full understanding of recursion and it's implementation
ixaxaar
@ixaxaar
Why scala? would it be more easier to say play around with Agsy of agda given now there also exists agda-cubical and haskell-torch to connect agda with neural networks for auto proof search?
ixaxaar
@ixaxaar
also could i attend some of your lectures without taking up a full time course? :grimacing:
I've been struggling with math for some time now and it would be interesting to take actual classes
some background -> https://www.reddit.com/r/math/comments/hli5lt/lost_in_pure_math_need_direction/
Siddhartha Gadgil
@siddhartha-gadgil
I need a general purpose language since I don't know what I am going to try. Perhaps the special way is better for something, even for everything
Siddhartha Gadgil
@siddhartha-gadgil
Also my lectures in the next semester will be online, so you are welcome to watch
ixaxaar
@ixaxaar
I have been working through some of the assignments, thats how I came to know of this proving-ground, thank you so much for putting them up online!
Also if you meant next semester's lecture recordings that would be amazing, thank you!
Dmytro Mitin
@DmytroMitin
@siddhartha-gadgil would you publish ProvingGround for 2.13? https://mvnrepository.com/artifact/io.github.siddhartha-gadgil
Siddhartha Gadgil
@siddhartha-gadgil
@DmytroMitin I have not published for a while. I shoud do so (I have very little experience with SonaType)
Siddhartha Gadgil
@siddhartha-gadgil
@DmytroMitin just published I hope, and it was easy this time (assuming it worked). The last time I had to set up a PGP key and so on. Being a mathematician largely self-taught in programming, I am wary of build, publish and such tasks.
Dmytro Mitin
@DmytroMitin
Thank you.
Peng Cheng
@tribbloid

@siddhartha-gadgil Thanks a lot for publishing, this is how I envision math should be done in the future.

I found 2 possible issues, wondering if you have co-maintainers that can take over some grunt works like build, publish and cross-environment checking:

  • 2 temporary directories .bsp and project/.bloop were committed into master, the generated files inside are only for your build environment (e.g. contains "/home/gadgil/")
  • tut is abandonware (https://github.com/tpolecat/tut) and can't be used to generate doc any longer

The project is used for both teaching and prototyping, which makes it kind of difficult to manage release

Siddhartha Gadgil
@siddhartha-gadgil
Thanks @tribbloid - I have removed the .bsp and project/.bloop. I do not really use tut even though there are files in the format of tut. I instead usemdoc` programmatically to generate the tutorials. That said, the tutorial generation (and many other things) are not well maintained.
Peng Cheng
@tribbloid

thanks a lot! On IntelliJ IDEA the bsp automatically chose mill as the build backend. Then it emits an error:

scalac: Output path /home/peng/git-release/ProvingGround/out/jvmRoot/compile/dest/classes is shared between: Module '(jvm+jvmcore)(Root) (shared)' production, Module '(jvm+leanlib)(Root+.)((js+jvm)) (shared)' production, Module '(jvm+mantle)(Root) (shared)' production, Module '(jvm+nlp)(Root) (shared)' production, Module '(jvm+server)(Root) (shared)' productionPlease configure separate output paths to proceed with the compilation.
TIP: you can use Project Artifacts to combine compiled classes if needed.

I wonder if mill is the recommended backend of the WIP master? Do you have to maintain 2 parallel build scripts?

Peng Cheng
@tribbloid
SORRY FALSE ALARM, IDEA imported the project twice in different mode
Peng Cheng
@tribbloid
Also, .bsppattern should be in your .gitignore