{"id":45884,"date":"2023-04-08T11:08:25","date_gmt":"2023-08-03T06:47:03","guid":{"rendered":"https:\/\/www.silicloud.com\/zh\/blog\/45884-2\/"},"modified":"2024-04-29T22:31:49","modified_gmt":"2024-04-29T14:31:49","slug":"45884-2","status":"publish","type":"post","link":"https:\/\/www.silicloud.com\/zh\/blog\/45884-2\/","title":{"rendered":""},"content":{"rendered":"<h1>1. \u6982\u8981<\/h1>\n<p>\u4ee5\u4e0b\u306e\u74b0\u5883\u3067Jupyter\u4e0a\u3067Coq\u304c\u4f7f\u3048\u308b\u74b0\u5883\u3092\u69cb\u7bc9\u3059\u308b\u3002<br \/>\n\uff08Anaconda\u306f\u4f7f\u308f\u306a\u3044\uff09<\/p>\n<ul class=\"post-ul\">\n<li style=\"list-style-type: none;\">\n<ul class=\"post-ul\">macOS Catalina<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n<ul class=\"post-ul\">\n<li style=\"list-style-type: none;\">\n<ul class=\"post-ul\">Homebrew<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n<ul class=\"post-ul\">\n<li style=\"list-style-type: none;\">\n<ul class=\"post-ul\">Python3<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n<ul class=\"post-ul\">\n<li style=\"list-style-type: none;\">\n<ul class=\"post-ul\">Jupyter<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n<ul class=\"post-ul\">Coq 8.10.0<\/ul>\n<h1>2. \u30bd\u30d5\u30c8\u30a6\u30a7\u30a2\u306e\u30a4\u30f3\u30b9\u30c8\u30fc\u30eb\u3068\u521d\u671f\u5316<\/h1>\n<p>brew\u306e\u30a4\u30f3\u30b9\u30c8\u30fc\u30eb\u306f\u3053\u306e\u30da\u30fc\u30b8\u3092\u53c2\u7167\u3002<br \/>\nHomebrew<\/p>\n<p>\u4ee5\u4e0b\u306e\u30b3\u30de\u30f3\u30c9\u3092\u5b9f\u884c\u3059\u308b\u3002<\/p>\n<pre class=\"post-pre\"><code>brew update\r\nbrew upgrade\r\nbrew install python3\r\nbrew install coq\r\npip3 install --upgrade pip\r\npip3 install jupyter\r\npip3 install coq-jupyter\r\npython3 -m coq_jupyter.install\r\n<\/code><\/pre>\n<h1>3. Jupyter notebook\u306e\u8d77\u52d5<\/h1>\n<p>\u4ee5\u4e0b\u306e\u30b3\u30de\u30f3\u30c9\u3092\u5b9f\u884c\u3059\u308b\u3002<\/p>\n<pre class=\"post-pre\"><code>jupyter notebook\r\n<\/code><\/pre>\n<p>\u30d6\u30e9\u30a6\u30b6\u304b\u3089localhost:8888\u3092\u30a2\u30af\u30bb\u30b9\u3059\u308b\u3068\u3001Jupyter\u3092\u8d77\u52d5\u3057\u305f\u30c7\u30a3\u30ec\u30af\u30c8\u30ea\u306e\u30d5\u30a1\u30a4\u30eb\u4e00\u89a7\u304c\u8868\u793a\u3055\u308c\u308b\u3002Mac\u7248\u306eJupyter\u3067\u306f\u3001\u30c7\u30d5\u30a9\u30eb\u30c8\u8a2d\u5b9a\u3067\u30ed\u30b0\u30a4\u30f3\u753b\u9762\u306f\u8868\u793a\u3055\u308c\u306a\u3044\u3002<\/p>\n<h1>4. \u4ed8\u9332<\/h1>\n<h2>4.1 \u30c1\u30e5\u30fc\u30c8\u30ea\u30a2\u30eb\u306e\u53d6\u5f97<\/h2>\n<p>Coq\u306e\u30c1\u30e5\u30fc\u30c8\u30ea\u30a2\u30eb\u3092clone\u3067\u3068\u3063\u3066\u304f\u308b\u3002\u305d\u306e\u30c7\u30a3\u30ec\u30af\u30c8\u30ea\u4e0b\u3067jupyter\u3092\u8d77\u52d5\u3059\u308b\u3068\u4fbf\u5229\u3002<\/p>\n<pre class=\"post-pre\"><code>git clone https:\/\/github.com\/maruyama097\/coq-tutorial.git\r\ncd coq-turorial\r\njupyter notebook\r\n<\/code><\/pre>\n<h2>4.2 Jupyter Lab\u306e\u5c0e\u5165<\/h2>\n<p>\u4ee5\u4e0b\u306e\u624b\u9806\u3067Jupyter Lab\u3092\u30a4\u30f3\u30b9\u30c8\u30fc\u30eb\u3001\u8d77\u52d5\u3059\u308b\u3053\u3068\u304c\u3067\u304d\u308b\u3002<br \/>\nJupyter Lab\u304b\u3089Coq\u3092\u4f7f\u7528\u3067\u304d\u308b\u3002<\/p>\n<pre class=\"post-pre\"><code>pip3 install jupyterlab\r\njupyter lab\r\n<\/code><\/pre>\n<p>\u4ee5\u4e0a<\/p>\n","protected":false},"excerpt":{"rendered":"<p>1. \u6982\u8981 \u4ee5\u4e0b\u306e\u74b0\u5883\u3067Jupyter\u4e0a\u3067Coq\u304c\u4f7f\u3048\u308b\u74b0\u5883\u3092\u69cb\u7bc9\u3059\u308b\u3002 \uff08Anaconda\u306f\u4f7f\u308f\u306a\u3044\uff09 ma [&hellip;]<\/p>\n","protected":false},"author":11,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[1],"tags":[],"class_list":["post-45884","post","type-post","status-publish","format-standard","hentry","category-uncategorized"],"yoast_head":"<!-- This site is optimized with the Yoast SEO Premium plugin v21.5 (Yoast SEO v21.5) - https:\/\/yoast.com\/wordpress\/plugins\/seo\/ -->\n<title>- Blog - Silicon Cloud<\/title>\n<meta name=\"robots\" content=\"index, follow, max-snippet:-1, max-image-preview:large, max-video-preview:-1\" \/>\n<link rel=\"canonical\" href=\"https:\/\/www.silicloud.com\/zh\/blog\/45884-2\/\" \/>\n<meta property=\"og:locale\" content=\"zh_CN\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:description\" content=\"1. \u6982\u8981 \u4ee5\u4e0b\u306e\u74b0\u5883\u3067Jupyter\u4e0a\u3067Coq\u304c\u4f7f\u3048\u308b\u74b0\u5883\u3092\u69cb\u7bc9\u3059\u308b\u3002 \uff08Anaconda\u306f\u4f7f\u308f\u306a\u3044\uff09 ma [&hellip;]\" \/>\n<meta property=\"og:url\" content=\"https:\/\/www.silicloud.com\/zh\/blog\/45884-2\/\" \/>\n<meta property=\"og:site_name\" content=\"Blog - Silicon Cloud\" \/>\n<meta property=\"article:published_time\" content=\"2023-08-03T06:47:03+00:00\" \/>\n<meta property=\"article:modified_time\" content=\"2024-04-29T14:31:49+00:00\" \/>\n<meta name=\"author\" content=\"\u65b0, \u97f5\" \/>\n<meta name=\"twitter:card\" content=\"summary_large_image\" \/>\n<meta name=\"twitter:label1\" content=\"\u4f5c\u8005\" \/>\n\t<meta name=\"twitter:data1\" content=\"\u65b0, \u97f5\" \/>\n<script type=\"application\/ld+json\" class=\"yoast-schema-graph\">{\"@context\":\"https:\/\/schema.org\",\"@graph\":[{\"@type\":\"WebPage\",\"@id\":\"https:\/\/www.silicloud.com\/zh\/blog\/45884-2\/\",\"url\":\"https:\/\/www.silicloud.com\/zh\/blog\/45884-2\/\",\"name\":\"- Blog - Silicon Cloud\",\"isPartOf\":{\"@id\":\"https:\/\/www.silicloud.com\/zh\/blog\/#website\"},\"datePublished\":\"2023-08-03T06:47:03+00:00\",\"dateModified\":\"2024-04-29T14:31:49+00:00\",\"author\":{\"@id\":\"https:\/\/www.silicloud.com\/zh\/blog\/#\/schema\/person\/4ba4019495123db3038fd0809e6959c9\"},\"inLanguage\":\"zh-Hans\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\/\/www.silicloud.com\/zh\/blog\/45884-2\/\"]}]},{\"@type\":\"WebSite\",\"@id\":\"https:\/\/www.silicloud.com\/zh\/blog\/#website\",\"url\":\"https:\/\/www.silicloud.com\/zh\/blog\/\",\"name\":\"Blog - Silicon Cloud\",\"description\":\"\",\"inLanguage\":\"zh-Hans\"},{\"@type\":\"Person\",\"@id\":\"https:\/\/www.silicloud.com\/zh\/blog\/#\/schema\/person\/4ba4019495123db3038fd0809e6959c9\",\"name\":\"\u65b0, \u97f5\",\"image\":{\"@type\":\"ImageObject\",\"inLanguage\":\"zh-Hans\",\"@id\":\"https:\/\/www.silicloud.com\/zh\/blog\/#\/schema\/person\/image\/\",\"url\":\"https:\/\/secure.gravatar.com\/avatar\/d484b6c6e4ae82e8a9efea989e1d2af46d9b6ef128101e63b18f559fca0ae627?s=96&d=mm&r=g\",\"contentUrl\":\"https:\/\/secure.gravatar.com\/avatar\/d484b6c6e4ae82e8a9efea989e1d2af46d9b6ef128101e63b18f559fca0ae627?s=96&d=mm&r=g\",\"caption\":\"\u65b0, \u97f5\"},\"url\":\"https:\/\/www.silicloud.com\/zh\/blog\/author\/yunxin\/\"},{\"@type\":\"ImageObject\",\"inLanguage\":\"zh-Hans\",\"@id\":\"https:\/\/www.silicloud.com\/zh\/blog\/45884-2\/#local-main-organization-logo\",\"url\":\"\",\"contentUrl\":\"\",\"caption\":\"Blog - Silicon Cloud\"}]}<\/script>\n<!-- \/ Yoast SEO Premium plugin. -->","yoast_head_json":{"title":"- Blog - Silicon Cloud","robots":{"index":"index","follow":"follow","max-snippet":"max-snippet:-1","max-image-preview":"max-image-preview:large","max-video-preview":"max-video-preview:-1"},"canonical":"https:\/\/www.silicloud.com\/zh\/blog\/45884-2\/","og_locale":"zh_CN","og_type":"article","og_description":"1. \u6982\u8981 \u4ee5\u4e0b\u306e\u74b0\u5883\u3067Jupyter\u4e0a\u3067Coq\u304c\u4f7f\u3048\u308b\u74b0\u5883\u3092\u69cb\u7bc9\u3059\u308b\u3002 \uff08Anaconda\u306f\u4f7f\u308f\u306a\u3044\uff09 ma [&hellip;]","og_url":"https:\/\/www.silicloud.com\/zh\/blog\/45884-2\/","og_site_name":"Blog - Silicon Cloud","article_published_time":"2023-08-03T06:47:03+00:00","article_modified_time":"2024-04-29T14:31:49+00:00","author":"\u65b0, \u97f5","twitter_card":"summary_large_image","twitter_misc":{"\u4f5c\u8005":"\u65b0, \u97f5"},"schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"WebPage","@id":"https:\/\/www.silicloud.com\/zh\/blog\/45884-2\/","url":"https:\/\/www.silicloud.com\/zh\/blog\/45884-2\/","name":"- Blog - Silicon Cloud","isPartOf":{"@id":"https:\/\/www.silicloud.com\/zh\/blog\/#website"},"datePublished":"2023-08-03T06:47:03+00:00","dateModified":"2024-04-29T14:31:49+00:00","author":{"@id":"https:\/\/www.silicloud.com\/zh\/blog\/#\/schema\/person\/4ba4019495123db3038fd0809e6959c9"},"inLanguage":"zh-Hans","potentialAction":[{"@type":"ReadAction","target":["https:\/\/www.silicloud.com\/zh\/blog\/45884-2\/"]}]},{"@type":"WebSite","@id":"https:\/\/www.silicloud.com\/zh\/blog\/#website","url":"https:\/\/www.silicloud.com\/zh\/blog\/","name":"Blog - Silicon Cloud","description":"","inLanguage":"zh-Hans"},{"@type":"Person","@id":"https:\/\/www.silicloud.com\/zh\/blog\/#\/schema\/person\/4ba4019495123db3038fd0809e6959c9","name":"\u65b0, \u97f5","image":{"@type":"ImageObject","inLanguage":"zh-Hans","@id":"https:\/\/www.silicloud.com\/zh\/blog\/#\/schema\/person\/image\/","url":"https:\/\/secure.gravatar.com\/avatar\/d484b6c6e4ae82e8a9efea989e1d2af46d9b6ef128101e63b18f559fca0ae627?s=96&d=mm&r=g","contentUrl":"https:\/\/secure.gravatar.com\/avatar\/d484b6c6e4ae82e8a9efea989e1d2af46d9b6ef128101e63b18f559fca0ae627?s=96&d=mm&r=g","caption":"\u65b0, \u97f5"},"url":"https:\/\/www.silicloud.com\/zh\/blog\/author\/yunxin\/"},{"@type":"ImageObject","inLanguage":"zh-Hans","@id":"https:\/\/www.silicloud.com\/zh\/blog\/45884-2\/#local-main-organization-logo","url":"","contentUrl":"","caption":"Blog - Silicon Cloud"}]}},"_links":{"self":[{"href":"https:\/\/www.silicloud.com\/zh\/blog\/wp-json\/wp\/v2\/posts\/45884","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.silicloud.com\/zh\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.silicloud.com\/zh\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.silicloud.com\/zh\/blog\/wp-json\/wp\/v2\/users\/11"}],"replies":[{"embeddable":true,"href":"https:\/\/www.silicloud.com\/zh\/blog\/wp-json\/wp\/v2\/comments?post=45884"}],"version-history":[{"count":2,"href":"https:\/\/www.silicloud.com\/zh\/blog\/wp-json\/wp\/v2\/posts\/45884\/revisions"}],"predecessor-version":[{"id":88034,"href":"https:\/\/www.silicloud.com\/zh\/blog\/wp-json\/wp\/v2\/posts\/45884\/revisions\/88034"}],"wp:attachment":[{"href":"https:\/\/www.silicloud.com\/zh\/blog\/wp-json\/wp\/v2\/media?parent=45884"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.silicloud.com\/zh\/blog\/wp-json\/wp\/v2\/categories?post=45884"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.silicloud.com\/zh\/blog\/wp-json\/wp\/v2\/tags?post=45884"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}